Utilisation de l'inégalité de type dans la programmation au niveau du type dans Haskell

Question

J'essaie d'effectuer une programmation avancée au niveau du type; l'exemple est une version réduite de mon programme original.

J'ai une représentation des types (Haskell). Dans cet exemple, je ne couvre que les types de fonctions, les types de base et les variables de type.

La représentation Type t est paramétrée par une variable de type t pour permettre également une différenciation sur le niveau type. Pour y parvenir, j'utilise principalement des GADT. Différents types et variables de type sont différenciés en utilisant des littéraux au niveau du type, ainsi la contrainte KnownSymbol et l'utilisation de 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) 

J'ai également limité le genre de t être de type TypeKind en utilisant les extensions DataKinds et KindSignatures et définir le type de données TypeKind:

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

Maintenant, je veux mettre en œuvre des substitutions de type variables, c'est-à-dire en substituant, dans un type t, chaque variable qui est égale à une variable de type y, avec le type t'. La substitution doit être implémentée sur la représentation, ainsi que sur le niveau type. Pour ce dernier, nous avons besoin 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) 

Les variables de type sont la partie intéressante, parce que nous vérifions pour l'égalité des symboles x et y au niveau du type. Pour cela, nous avons également besoin d'un (poly-kinded) le type de famille qui nous permet de choisir entre deux résultats:

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

Malheureusement, cela ne compile pas encore, ce qui pourrait être le premier indicateur de mon problème:

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’ 

Activation de l'extension UndecidableInstances fonctionne, bien que, si nous continuons à définir une fonction subst qui fonctionne sur la valeur de niveau:

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 

Cette code fonctionne parfaitement, à l'exception de la dernière ligne qui produit l'erreur de compilation suivante:

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 

Je suppose que le problème est que je ne peux pas prouver l'inégalité des types des deux symboles x et y, et aurais besoin type de témoin de type-inégalité. Est-ce possible? Ou y a-t-il une autre meilleure façon d'atteindre mon objectif? Je ne sais pas dans quelle mesure les questions 'idiomatic' Haskell type inequality et Can GADTs be used to prove type inequalities in GHC? répondent déjà à ma question. Toute aide serait appréciée.

Answer 1

Comme l'a dit chi dans les commentaires, ce dont vous avez besoin est Either ((x==y) :~: True) ((x==y) :~: False). Malheureusement, les littéraux de type sont en partie cassés actuellement, et c'est l'une des choses que nous ne pouvons faire qu'avec unsafeCoerce (une utilisation moralement acceptable cependant).

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 

Sur une autre note, si cela ne vous dérange pas un modèle Haskell, la bibliothèque singletons peut déduire vos définitions (et plus):

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

Cela nous donne le type, les définitions de niveau nature et de valeur pour Type et subst. Exemples:

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