haskell - 在 Haskell 的类型级编程中使用类型不等式

Question

我正在尝试进行一些高级类型级编程；该示例是我的原始程序的简化版本。

我有(Haskell)类型的表示。在这个例子中我只介绍函数类型、基本类型和类型变量。

表示Type t由一个类型变量 t 参数化还允许在类型级别上进行区分。为了实现这一点，我主要使用 GADT。不同的类型和类型变量通过使用类型级别文字来区分，因此 KnownSymbol约束和使用Proxy s。

{-# LANGUAGE GADTs, TypeOperators, DataKinds, KindSignatures, TypeFamilies, PolyKinds #-}

import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality

data Type :: TypeKind -> * where
  TypeFun    :: Type a -> Type b -> Type (a :-> b)
  Type       :: KnownSymbol t => Proxy t -> Type (Ty t)
  TypeVar    :: KnownSymbol t => Proxy t -> Type (TyVar t)

我还限制了 t 的类型友善TypeKind通过使用 DataKinds 和 KindSignatures 扩展并定义 TypeKind数据类型:

data TypeKind =
    Ty Symbol
  | TyVar Symbol
  | (:->) TypeKind TypeKind

现在我想实现类型变量的替换，即在类型 t 内进行替换，每个变量x等于类型变量 y ，类型为t' 。替换必须在表示以及类型级别上实现。对于后者，我们需要 TypeFamilies:

type family Subst (t :: TypeKind) (y :: Symbol) (t' :: TypeKind) :: TypeKind where
  Subst (Ty t) y t'    = Ty t
  Subst (a :-> b) y t' = Subst a y t' :-> Subst b y t'
  Subst (TyVar x) y t' = IfThenElse (x == y) t' (TyVar x)

类型变量是有趣的部分，因为我们检查符号 x 的相等性和y在类型级别上。为此，我们还需要一个(多类)类型族，它允许我们在两个结果之间进行选择:

type family IfThenElse (b :: Bool) (x :: k) (y :: k) :: k where
  IfThenElse True  x y = x
  IfThenElse False x y = y

不幸的是，这还没有编译，这可能是我的问题的第一个指标:

Nested type family application
  in the type family application: IfThenElse (x == y) t' ('TyVar x)
(Use UndecidableInstances to permit this)
In the equations for closed type family ‘Subst’
In the type family declaration for ‘Subst’

不过，启用 UndecidableInstances 扩展是有效的，因此我们继续定义一个函数 subst适用于值(value)级别:

subst :: (KnownSymbol y) => Type t -> Proxy (y :: Symbol) -> Type t' -> Type (Subst t y t')
subst (TypeFun a b) y t = TypeFun (subst a y t) (subst b y t)
subst t@(Type _) _ _    = t
subst t@(TypeVar x) y t'
  | Just Refl <- sameSymbol x y = t'
  | otherwise                   = t

这段代码工作完美，除了最后一行产生以下编译错误:

Could not deduce (IfThenElse
                    (GHC.TypeLits.EqSymbol t1 y) t' ('TyVar t1)
                  ~ 'TyVar t1)
from the context (t ~ 'TyVar t1, KnownSymbol t1)
  bound by a pattern with constructor
             TypeVar :: forall (t :: Symbol).
                        KnownSymbol t =>
                        Proxy t -> Type ('TyVar t),
           in an equation for ‘subst’
  at Type.hs:29:10-18
Expected type: Type (Subst t y t')
  Actual type: Type t
Relevant bindings include
  t' :: Type t' (bound at Type.hs:29:23)
  y :: Proxy y (bound at Type.hs:29:21)
  x :: Proxy t1 (bound at Type.hs:29:18)
  subst :: Type t -> Proxy y -> Type t' -> Type (Subst t y t')
    (bound at Type.hs:27:1)
In the expression: t
In an equation for ‘subst’:
    subst t@(TypeVar x) y t'
      | Just Refl <- sameSymbol x y = t'
      | otherwise = t

我猜问题是我无法证明两个符号的类型不相等x和y ，并且需要某种类型不等式见证。这可能吗？或者还有其他更好的方法来实现我的目标吗？不知道问题到什么程度'idiomatic' Haskell type inequality和 Can GADTs be used to prove type inequalities in GHC?已经回答我的问题了。任何帮助将不胜感激。

Answer 1

正如 chi 在评论中所说，您需要的是 Either ((x==y) :~: True) ((x==y) :~: False)。不幸的是，类型文字目前有部分被破坏，这是我们只能使用 unsafeCoerce 做的事情之一(尽管在道德上是可以接受的用途)。

sameSymbol' ::
  (KnownSymbol s, KnownSymbol s') =>
  Proxy s -> Proxy s'
  -> Either ((s == s') :~: True) ((s == s') :~: False)
sameSymbol' s s' = case sameSymbol s s' of
  Just Refl -> Left Refl
  Nothing   -> Right (unsafeCoerce Refl)

subst :: (KnownSymbol y) => Type t -> Proxy (y :: Symbol) -> Type t' -> Type (Subst t y t')
subst (TypeFun a b) y t = TypeFun (subst a y t) (subst b y t)
subst t@(Type _) _ _    = t
subst t@(TypeVar x) y t' = case sameSymbol' x y of
  Left  Refl -> t'
  Right Refl -> t

另一方面，如果您不介意一些 Haskell 模板，则 singletons库可以导出您的定义(以及更多):

{-# language GADTs, TypeOperators, DataKinds, KindSignatures, TypeFamilies, PolyKinds #-}
{-# language UndecidableInstances, ScopedTypeVariables, TemplateHaskell, FlexibleContexts #-}

import GHC.TypeLits
import Data.Singletons.TH
import Data.Singletons.Prelude

singletons([d|
  data Type sym
    = Ty sym
    | TyVar sym
    | Type sym :-> Type sym

  subst :: Eq sym => Type sym -> sym -> Type sym -> Type sym
  subst (Ty t) y t'    = Ty t
  subst (a :-> b) y t' = subst a y t' :-> subst b y t'
  subst (TyVar x) y t' = if x == y then t' else TyVar x        
  |])

这为我们提供了 Type 和 subst 的类型、种类和值级别定义。示例:

-- some examples

-- type level
type T1 = Ty "a" :-> TyVar "b"
type T2 = Subst T1 "b" (Ty "c") -- this equals (Ty "a" :-> Ty "c")

-- value level

-- automatically create value-level representation of T1
t1  = sing :: Sing T1

-- or write it out by hand
t1' = STy (sing :: Sing "a") :%-> STyVar (sing :: Sing "b")

-- use value-level subst on t1:
t2 = sSubst t1 (sing :: Sing "b") (STy (sing :: Sing "c"))

-- or generate result from type-level representation
t2' = sing :: Sing (Subst T1 "b" (Ty "c"))

-- Convert singleton to non-singleton (and print it)
t3 :: Type String
t3 = fromSing t2 -- Ty "a" :-> Ty "c"