Haskellの型レベルプログラミングで型不等式を使用する

Question

高度な型レベルプログラミングをしようとしています。この例は私の元のプログラムの縮小バージョンです。

私は（ハスケル）型の表現をしています。この例では、関数型、基本型、型変数のみを扱います。

表現Type tは、1つのタイプ変数tによってパラメータ化され、タイプレベルの差別化も可能です。これを達成するために、主にGADTを使用しています。異なる型と型変数は、型レベルのリテラルを使用することによって区別されるため、KnownSymbol制約とProxyの使用が区別されます。

{-# 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データ型を定義することによって、一種TypeKindであることがtの種類をも制限されている：

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

今、私はタイプの置換を実装します変数、すなわちタイプtの中で、変数xをタイプ変数yのタイプt'と等しいすべての変数に置き換えます。代入は、表現およびタイプレベルで実装されなければなりません。後者の場合、我々はTypeFamilies必要があります：私たちはタイプレベルのシンボルxとyの平等をチェックするため

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) 

を型変数は、興味深い部分です。このために、我々はまた、（ポリkinded）を必要とする私たちは二つの結果の間で選択することができます家族のように入力します。

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

残念ながら、これは私の問題の最初の指標であるかもしれない、まだコンパイルされません。

UndecidableInstances拡張を有効にする

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’ 

は、しかし、働くので、私たちは価値のレベルで動作する機能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 

私はこの問題は、私は2つのシンボルxとyの種類の不平等を証明することができないということであり、いくつかの必要があると思います型不平等証人の一種。これは可能ですか？または、私の目標を達成するための別の方法がありますか？ 質問'idiomatic' Haskell type inequalityとCan GADTs be used to prove type inequalities in GHC?がすでに私の質問にどの程度回答しているかわかりません。どんな助けもありがとう。

Answer 1

あなたが必要とするのは、コメントに記載されているとおり、Either ((x==y) :~: True) ((x==y) :~: False)です。残念ながら、タイプリテラルは現在部分的に解消されており、これはunsafeCoerce（ただし、道徳的には許容されていますが）でしかできないものの1つです。別のノートで

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"