在运行时输入带有存在的杂耍

Question

我正在玩Haskell中的存在感和GADT,我正在尝试为组合器定义DSL(例如SKI).我有GADT工作,以及一个工作正常的减少功能(并且与问题无关)

{-# LANGUAGE GADTs, ExistentialQuantification #-}

import Control.Applicative
import Data.Monoid
import Control.Monad

data Comb t where
    S :: Comb ((a -> b -> c) -> (a -> b) -> a -> c)
    K :: Comb (a -> b -> a)
    I :: Comb (a -> a)
    B :: Comb ((b -> c) -> (a -> b) -> a -> c)
    C :: Comb ((b -> a -> c) -> a -> b -> c)
    W :: Comb ((a -> a -> b) -> a -> b)
    (:$) :: Comb (a -> b) -> Comb a -> Comb b

我现在要做的是定义一种在运行时从用户读取组合字符串的方法.显然,我需要一个存在类型来执行此操作,因为需要隐藏GADT的类型信息.

data CombBox = forall a. CombBox { unCombBox :: Comb a }

($$) :: CombBox -> CombBox -> Maybe CombBox
x $$ y = undefined -- ???

我希望($$)函数能够以某种方式"查看" CombBox运行时的存在性,如果有可能将两个组合使用:$并得到一个良好类型的结果,我希望结果是这样的.否则,我想要Nothing.所以,例如,

CombBox S $$ CombBox K ==> Just (CombBox (S :$ K))
CombBox W $$ CombBox I ==> Nothing

后者应该失败,因为W期望2-ary函数I需要一个参数.但是我想把这个检查放到运行时,我不确定在Haskell(+ GHC扩展)类型系统中是否可以这样做.

Answer 1

准备好了解依赖对和单身人士!

我将稍微改写你的系统以简化它.

首先,我将把所有类型的宇宙从所有Haskell缩小到一个更简单的宇宙,由一个原始类型和箭头组成.

infixr 0 :->
data Type = Unit | Type :-> Type

希望您应该能够看到如何使用更原始的类型扩展它.

我也将删除大部分比特Comb,因为它们都可以相互表达.

data Comb a where
    S :: Comb ((a :-> b :-> c) :-> (a :-> b) :-> a :-> c)
    K :: Comb (a :-> b :-> a)
    (:$) :: Comb (a :-> b) -> Comb a -> Comb b

i = S :$ K :$ i
b = (S :$ (K :$ S)) :$ K
c = S :$ (S :$ (K :$ (S :$ (K :$ S) :$ K)) :$ S) :$ (K :$ K)
w = S :$ S :$ (S :$ K)

现在回答你的问题.正如您正确推测的那样,当您正在阅读用户输入时,您无法静态地预测结果术语的类型,因此您需要对其进行存储量化.

data Ex f = forall a. Ex (f a)

问题是:如何恢复类型信息以便能够操纵术语？我们可以将a Comb与您可以在运行时进行模式匹配的另一个值配对,以了解其类型Comb.这是一个用于配对的组合器.

data (f :*: g) i = f i :*: g i

(我把这些类型从该Hasochism纸.):*:对两种类型的保证,他们的指数都是平等的.我们将它与Ex模拟依赖对或西格玛类型一起使用:一对值,第二个组件的类型取决于第一个组件的值.我的想法是,f它将是一个GADT,告诉你它的索引,所以模式匹配f为你提供有关类型的信息g.

type Sg f g = Ex (f :*: g)
pattern Sg x y = Ex (x :*: y)

现在聪明的部分:提出一个GADT,告诉你一个组合词的类型.

data Typey t where
    Unity :: Typey Unit
    Arry :: Typey a -> Typey b -> Typey (a :-> b)

Typey被称为单身人士.对于给定的t,只存在一个类型的值Typey t.因此,如果您Typey t有价值,您就会知道所有需要了解的内容t.

单身人士价值最终是一个黑客.Typey不是Type; 它Type是重复类型级副本的价值级替身.在一个真正依赖类型的系统中,你不需要使用单独的胶水将值级别的东西粘贴到类型级别的东西,因为首先不存在区别.

我们的存在量化组合现在看起来像这样.AComb打包一个Comb具有其类型的运行时表示.这种技术使我们能够保证盒装Comb是好的; 我们不能静态地说那种类型是什么.

type AComb = Sg Typey Comb

我们如何写($$),试图应用于AComb另一个AComb？我们需要对其关联的Typeys 进行模式匹配,以便了解是否可以将一个应用于另一个.特别是,我们需要一种方法来了解两种类型是否相等.

这就是命题平等,一个GADT证明两个类型级别的东西是平等的.Refl如果您可以向GHC解释a并且b实际上是相同的,那么您只能给出一个值.相反,如果你模式匹配,Refl那么GHC将添加a ~ b到输入上下文.

data a :~: b where
    Refl :: a :~: a
withEq :: a :~: b -> (a ~ b => r) -> r
withEq Refl x = x

这是一个辅助函数,通过:->构造函数提升一对等式.

arrEq :: (a :~: c) -> (b :~: d) -> (a :-> b) :~: (c :-> d)
arrEq Refl Refl = Refl

正如所承诺的,我们可以写下一个函数来检查两个Types是否相等.我们继续对它们的相关单例进行模式匹配Typey,如果我们发现类型不兼容则失败.如果相等测试成功,那么战利品就是类型相同的证明.

tyEq :: Typey t -> Typey u -> Maybe (t :~: u)
tyEq Unity Unity = Just Refl
tyEq (Arry a b) (Arry c d) = liftA2 arrEq (tyEq a c) (tyEq b d)
tyEq _ _ = Nothing

withTyEq :: Typey t -> Typey u -> (t ~ u => a) -> Maybe a
withTyEq t u x = fmap (\p -> withEq p x) (tyEq t u)

最后,我们可以写$$.输入规则如下:

f : a -> b    y : a
------------------- App
      f y : b

也就是说,如果左手术语$$是函数类型,并且右手术语的类型与函数的域匹配,我们可以键入应用程序.因此,此规则的实现必须测试(使用withTyEq)相关类型是否匹配才能返回结果项.

($$) :: AComb -> AComb -> Maybe AComb
Sg (Arry a b) x $$ Sg t y = withTyEq a t $ Sg b (x :$ y)
_ $$ _ = Nothing

生成Typey术语对应于类型检查的行为.换句话说,函数parse :: String -> AComb必须同时进行解析和类型检查.在实际的编译器中,这两个阶段是分开的.

因此,我建议将用户输入解析为无类型语法树,该语法树允许格式错误的术语,然后单独生成键入信息.

data Expr = S | K | Expr :$ Expr
parse :: String -> Parser Expr
typeCheck :: Expr -> Maybe AComb

一个有趣的练习(在更依赖类型的语言中)是修改typeCheck以返回更详细的解释为什么类型检查失败的原因,比如这个伪Agda:

data Void : Set where
Not : Set -> Set
Not a = a -> Void

data TypeError : Expr -> Set where
    notArr : Not (IsFunction f) -> TypeError (f :$ x)
    mismatch : Not (domain f :~: type x) -> TypeError (f :$ x)
    inFunc : TypeError f -> TypeError (f :$ x)
    inArg : TypeError x -> TypeError (f :$ x)

typeCheck : (e : Expr) -> Either (TypeError e) AComb

您也可以typeCheck通过确保它不会改变您给出的术语(另一项练习)来更精确.

有关进一步阅读,请参阅左侧视图,其中包含经验证的lambda演算类型检查器.