Verwendung von Typ-Ungleichheit innerhalb der Typenebene Programmierung in Haskell

Question

Ich versuche, einige erweiterte Typ-Level-Programmierung zu tun; Das Beispiel ist eine reduzierte Version meines ursprünglichen Programms.

Ich habe eine Darstellung von (Haskell) Typen. In diesem Beispiel behandle ich nur Funktionstypen, Grundtypen und Typvariablen.

Die Darstellung Type t ist durch eine Typvariable t parametriert, um auch eine Unterscheidung auf der Typ-Ebene zu ermöglichen. Um dies zu erreichen, verwende ich hauptsächlich GADTs. Unterschiedliche Typen und Typvariablen werden unterschieden, indem Literale auf Typenebene verwendet werden, also die KnownSymbol Einschränkung und die Verwendung von 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) 

Ich habe beschränkt auch die Art der t von Art TypeKind sein, indem sie die DataKinds und KindSignatures Erweiterungen und Definition der TypeKind Datentyp:

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

Jetzt möchte ich Substitutionen von Typ implementieren Variablen, dh Ersetzen innerhalb einer Art t jede Variable x, die gleich einer Typvariable y ist, mit Typ t'. Die Substitution muss sowohl auf der Repräsentation als auch auf der Typ-Ebene implementiert werden. Für letzteren müssen wir 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) 

Die Typvariablen sind der interessante Teil, weil wir für die Gleichheit der Symbole überprüfen x und y auf der Typebene. Dafür brauchen wir auch einen (Poly-kinded) -Typ-Familie, die wir zwischen zwei Ergebnissen auswählen kann:

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

Leider kompiliert, dies noch nicht, was der erste Indikator für mein Problem sein könnte:

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’ 

die UndecidableInstances Erweiterung Aktivieren funktioniert, obwohl, so dass wir auch weiterhin eine Funktion subst definieren, die auf dem Wert-Ebene funktioniert:

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 

diese Code funktioniert perfekt, mit Ausnahme der letzten Zeile, das die folgenden Kompilierungsfehler erzeugt:

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 

Ich denke, dass das Problem ist, dass ich nicht die Ungleichheit der Typen der beiden Symbole x und y beweisen kann, und muß einig Art von Typ-Ungleichheit Zeuge. Ist das möglich? Oder gibt es einen anderen, besseren Weg, um mein Ziel zu erreichen? Ich weiß nicht, in welchem ​​Umfang die Fragen 'idiomatic' Haskell type inequality und Can GADTs be used to prove type inequalities in GHC? bereits meine Frage beantworten. Jede Hilfe wäre willkommen.

Answer 1

Wie Chi sagte in den Kommentaren, was Sie brauchen, ist Either ((x==y) :~: True) ((x==y) :~: False). Leider sind Typliterale zur Zeit teilweise gebrochen, und dies ist eines der Dinge, die wir nur mit unsafeCoerce (eine moralisch akzeptable Verwendung obwohl) tun können.

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 

Auf einer anderen Anmerkung, wenn Sie einige Template Haskell nichts dagegen, die singletons Bibliothek können Sie Ihre Definitionen (und mehr) ableiten:

{-# 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   
    |]) 

Dies gibt uns Art, Art und Wert-Level-Definitionen für Type und subst. Beispiele:

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