在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中，替换为类型变量y，类型为t'的每个变量x。替代必须在表示上以及在类型级别上执行。对于后者，我们需要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平等。对于这一点，我们还需要一个（聚kinded）型系列，可以让我们两个结果之间进行选择：

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上的价值层面的工作：

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 

在另一方面，如果你不介意一些模板哈斯克尔，该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"