在 Haskell 中的类型级编程中使用类型不等式
Using type-inequality within type-level programming in Haskell
我正在尝试进行一些高级类型级编程;该示例是我原始程序的简化版本。
我有 (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)
我还通过使用 DataKinds 和 KindSignatures 扩展并定义 TypeKind
数据类型,将 t
的种类限制为 TypeKind
种类:
data TypeKind =
Ty Symbol
| TyVar Symbol
| (:->) TypeKind TypeKind
现在我想实现类型变量的替换,即在类型 t
中,将等于类型变量 y
的每个变量 x
替换为类型 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
,它在值级别上起作用:
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 and Can GADTs be used to prove type inequalities in GHC? 在多大程度上已经回答了我的问题。任何帮助将不胜感激。
正如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"
我正在尝试进行一些高级类型级编程;该示例是我原始程序的简化版本。
我有 (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)
我还通过使用 DataKinds 和 KindSignatures 扩展并定义 TypeKind
数据类型,将 t
的种类限制为 TypeKind
种类:
data TypeKind =
Ty Symbol
| TyVar Symbol
| (:->) TypeKind TypeKind
现在我想实现类型变量的替换,即在类型 t
中,将等于类型变量 y
的每个变量 x
替换为类型 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
,它在值级别上起作用:
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 and Can GADTs be used to prove type inequalities in GHC? 在多大程度上已经回答了我的问题。任何帮助将不胜感激。
正如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"