Haskell 中的类型级环境

Question

我正在尝试使用一些 Haskell 扩展来实现简单的 DSL。我想要的一个功能是为变量提供类型级别的上下文。我知道这种事情在 Agda 或 Idris 等语言中很常见。但我想知道是否有可能在 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 来限制查找的类型。

我们也可以returnMaybe *。事实上，Data.Singletons.Prelude.List 中的 Lookup 就是这样做的，因此也可以使用它。但是，在类型级别上，我们通常可以使用部分函数，因为没有匹配大小写的类型系列应用程序会卡住而不是抛出错误，因此具有类型 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)的形状。您可以通过提供索引来证明某个项目在列表中。

为了编写 lambda 演算类型检查器，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

de Bruijn 索引对编译器编写者有很大的优势：它们很简单，你不必担心 alpha-equivalence，在这个例子中你不必乱搞类型级查找表或 Symbols。但是，即使有类型检查器的帮助，头脑正常的人也不会使用带有 de Bruijn 索引的语言进行编程。这使它们成为编译器中中间语言的不错选择，您可以将具有显式变量名的表面语言翻译成这种语言。

类型级环境和 de Bruijn 索引都相当复杂，所以您应该问问自己：谁是这种语言的目标受众？（以及：类型级环境值得付出代价吗？) 它是否是期望熟悉度、简单性和性能的嵌入式 DSL？如果是这样，我会考虑使用 higher-order abstract syntax. Or is it to be used as an intermediate language, for whom the primary audience is yourself, the compiler writer? Then I'd use a library like Kmett's bound 进行更深层次的嵌入来处理变量绑定并吸收类型错误的可能性，因为它们无论如何都可能发生。

有关类型级环境的更多信息等，请参阅 The View from the Left for (as far as I know) the first example of a statically-checked lambda calculus type-checker embedded in a dependently-typed programming language. Norell gives an Agda-flavoured exposition of the same program in the Agda tutorial and a series of lectures. See also this question，这似乎与您的用例相关。

Haskell 中的类型级环境

Type level environment in Haskell

haskell

dependent-type

type-level-computation