haskell - 在运行时使用存在类进行杂耍

Question

我正在Haskell中研究存在性和GADT，并且正在尝试为组合器（例如SKI）定义DSL。我有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元函数，其中 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)

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

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

（我从 the Hasochism paper删除了这两种类型。） :*:将两种类型配对以确保它们的索引相等。我们将其与 Ex一起使用，以模拟依赖对或sigma类型：一对值，第二个组件的类型取决于第一个组件的值。这个想法是 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的所有知识。

Singleton值最终是hack。 Typey不是 Type;它是 Type的重复类型级副本的值级替身。在真正的依存类型系统中，您不需要单例胶水就可以将价值级别的内容附加到类型级别的内容上，因为首先没有区别。

我们现有的量化组合器现在看起来像这样。 AComb用其类型的运行时表示包装 Comb。这种技术使我们能够保证框 Comb的类型正确；我们只是不能静态地说那是什么类型。

type AComb = Sg Typey Comb

我们如何编写 ($$)尝试将 AComb应用于另一个 AComb？我们需要在它们关联的 Typey上进行模式匹配，以了解是否可以将一个应用于另一个。特别是，我们将需要一种方法来知道两种类型是否相等。

命题相等，这是GADT证明两个类型层事物相等的证明。如果您可以向GHC解释 Refl和 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

如所承诺的，我们可以写下一个函数来检查两个 Type是否相等。我们对它们相关的单例 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不会改变您给它的用语来使它更精确（另一项练习）。

有关更多信息，请参见 The View from the Left，该功能具有经过验证的lambda演算类型检查器。