在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"