Тип уровня среды в Haskell

Question

Я пытаюсь использовать некоторые расширения Haskell для реализации простой DSL. Функция, которая мне нужна, это иметь контекст уровня типа для переменных. Я знаю, что это обычное место в таких языках, как Агда или Идрис. Но я хотел бы знать, можно ли добиться тех же результатов в Haskell.

Моя идея: использовать списки ассоциаций типов. Код выглядит следующим образом:

{-# LANGUAGE GADTs, 
     DataKinds, 
     PolyKinds, 
     TypeOperators, 
     TypeFamilies, 
     ScopedTypeVariables, 
     ConstraintKinds, 
     UndecidableInstances #-} 

import Data.Proxy  
import Data.Singletons.Prelude 
import Data.Singletons.Prelude.List 

import GHC.Exts  
import GHC.TypeLits 

type family In (s :: Symbol)(a :: *)(env :: [(Symbol, *)]) :: Constraint where 
    In x t '[] =() 
    In x t ('(y,t) ': env) = (x ~ y , In x t env) 


data Exp (env :: [(Symbol, *)]) (a :: *) where 
    Pure :: a -> Exp env a 
    Map :: (a -> b) -> Exp env a -> Exp env b   
    App :: Exp env (a -> b) -> Exp env a -> Exp env b   
    Set :: (KnownSymbol s, In s t env) => proxy s -> t -> Exp env() 
    Get :: (KnownSymbol s, In s t env) => proxy s -> Exp env t 


test :: Exp '[ '("a", Bool), '("b", Char) ] Char 
test = Get (Proxy :: Proxy "b")   

семейного типа In моделей типа списка уровень членства ограничений, который используется для того, чтобы переменная может быть использована только тогда, когда он находится на данной среде env.

Проблема заключается в том, что GHC решатель не может повлечь за собой ограничение In "b" Char [("a",Bool), ("b",Char)] для test функции, что дает следующее сообщение об ошибке:

Could not deduce (In "b" Char '['("a", Bool), '("b", Char)]) 
    arising from a use of ‘Get’ 
In the expression: Get (Proxy :: Proxy "b") 
In an equation for ‘test’: test = Get (Proxy :: Proxy "b") 
Failed, modules loaded: Main. 

Я использую GHC 7.10.3. Любой отзыв о том, как я могу решить это или объяснить, почему это невозможно, очень приветствуется.

Answer 1

In создает невозможные ограничения:

In "b" Char '['("a", Bool), '("b", Char)] = 
("b" ~ "a", ("b" ~ "b",()) 

Это соединение и оно имеет невозможный элемент "a" ~ "b", так что невозможно в целом.

Кроме того, ограничение не говорит нам ничего о Char, который я предполагаю, это искаженное значение.

Самый простой способ будет непосредственно с помощью функции просмотра:

type family Lookup (s :: Symbol) (env :: [(Symbol, *)]) :: * where 
    Lookup s ('(s , v) ': env) = v 
    Lookup s ('(s' , v) ': env) = Lookup s env 

Мы можем использовать Lookup k xs ~ val поставить ограничения на выглядели вверх типов.

Мы также можем вернуть Maybe *. Действительно, Lookup в Data.Singletons.Prelude.List делает это, чтобы его можно было использовать тоже. Тем не менее, на уровне типов мы часто можем получить частичные функции, так как типовые семейные приложения без подходящего случая застревают, а не бросают ошибки, поэтому наличие значения типа Lookup k xs :: * уже является достаточным доказательством того, что k действительно является ключом, содержащимся в xs ,

Answer 2

Ваш In - это не то, что вы думаете - это на самом деле больше похоже на All. Значение типа In x t xs является доказательством того, что каждый Элемент (тип-уровня) xs равен '(x,t).

Следующая GADT является более обычным доказательством членства:

data Elem x xs where 
    Here :: Elem x (x ': xs) 
    There :: Elem x xs -> Elem y (x ': xs) 

Elem, как натуральное число, но с большим количеством типов: сравнить форму There (There Here) с тем из S (S Z). Вы подтверждаете, что элемент находится в списке, указав его индекс.

В целях написания проверки типа лямбда-исчисления Elem полезен как de Bruijn index в виде типов (типа).

data Ty = NatTy | Ty ~> Ty 

data Term env ty where 
    Lit :: Nat -> Term env NatTy 
    Var :: Elem t env -> Term env t 
    Lam :: Term (u ': env) t -> Term env (u ~> t) 
    ($$) :: Term env (u ~> t) -> Term env u -> Term env t 

де Брейна индексы имеют большие преимущества для компиляторов: они просты, вам не нужно беспокоиться о alpha-equivalence, и в этом примере вы не должны возиться с таблицами типа уровня подстановок или Symbol s. Но никто в здравом уме никогда не будет программировать на языке с индексами Брюйна, даже с помощью проверки типа, чтобы помочь. Это делает их хорошим выбором для промежуточного языка в компиляторе, к которому вы переводили бы поверхностный язык с явными именами переменных.

Уровни уровня и индексы Bruijn являются довольно сложными, поэтому вы должны задать себе вопрос: кто является целевой аудиторией для этого языка? (и: - это система на уровне уровня, которая стоит затрат?) Является ли это встроенным DSL с ожиданием знакомости, простоты и производительности? Если это так, я бы рассмотрел более глубокое внедрение с использованием higher-order abstract syntax. Или он должен использоваться как промежуточный язык, для которого основная аудитория - это вы, автор компилятора? Затем я бы использовал библиотеку, например, Kmett's bound, чтобы позаботиться о привязке переменных и впитать возможность ошибок типа, потому что они могут случиться в любом случае.

Более подробной информации о средах типа уровня и др см The View from the Left для (насколько я знаю) первый пример статический проверяемой лямбда-исчисление типа-проверка, встроенная в типизированном зависимом от языка программирования. Norell дает экспозицию с такой же программой в Agda в the Agda tutorial и a series of lectures. См. Также this question, который кажется уместным для вашего прецедента.