Pourquoi GHC ne réduira-t-il pas ma famille de caractères?

Question

Voici un lambda-calcul non typé dont les termes sont indexés par leurs variables libres. J'utilise la bibliothèque singletons pour les valeurs singleton de chaînes de niveau de type. Un Var introduit une variable libre. Une abstraction lambda lie une variable qui apparaît libre dans le corps (s'il y en a une qui correspond). Les applications joignent les variables libres des deux parties de l'expression, supprimant les doublons (donc les variables libres de x y sont x et y, alors que les variables libres de x x sont juste). Je rédigeai ces types de familles:

type family Remove x xs where 
    Remove x '[] = '[] 
    Remove x (x ': xs) = Remove x xs 
    Remove x (y ': xs) = y ': Remove x xs 

type family Union xs ys where 
    Union xs ys = Nub (xs :++ ys) 

type family xs :++ ys where 
    '[] :++ ys = ys 
    (x ': xs) :++ ys = x ': (xs :++ ys) 

type family Nub xs where 
    Nub xs = Nub' '[] xs 

type family Nub' seen xs where 
    Nub' seen '[] = '[] 
    Nub' seen (x ': xs) = If (Elem x seen) (Nub' seen xs) (Nub' (x ': seen) (x ': xs)) 

type family If c t f where 
    If True t f = t 
    If False t f = f 

type family Elem x xs where 
    Elem x '[] = False 
    Elem x (x ': xs) = True 
    Elem x (y ': xs) = Elem x xs 

j'ai testé ceci à l'invite interactive:

ghci> :t Var (sing :: Sing "x") 
Var (sing :: Sing "x") :: Expr '["x"] -- good 
ghci> :t (Lam (sing :: Sing "x") (Var (sing :: Sing "x"))) 
(Lam (sing :: Sing "x") (Var (sing :: Sing "x"))) 
    :: Expr (Remove "x" '["x"]) -- not so good 

Je fus surpris d'apprendre que le type de la fonction d'identité \x. x est Expr (Remove "x" '["x"]), pas Expr '[]. GHC ne semble pas disposé à évaluer la famille de caractères Remove. J'ai expérimenté un peu plus et a appris que ce n'est pas un problème avec ma famille de type en tant que tel - GHC est heureux de le réduire dans ce cas:

ghci> :t (Proxy :: Proxy (Remove "x" '["x"])) 
(Proxy :: Proxy (Remove "x" '["x"])) :: Proxy '[] 

donc: Pourquoi ne GHC réduire Remove "x" '["x"] à '[] quand je interroger le type de mon GADT? En général, quand le vérificateur de type va-t-il ou ne va-t-il pas évaluer une famille de types? Y a-t-il des heuristiques que je peux utiliser pour éviter d'être surpris par son comportement?

Answer 1

Cela fonctionne. GHC semble être juste paresseux.

λ *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) 
(Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) 
    :: Expr (Remove "x" '["x"]) 

λ *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr '[] 
(Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr '[] 
    :: Expr '[] 

λ *Main > :t (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: Expr '["x"] 

<interactive>:1:2: 
    Couldn't match type ‘'[]’ with ‘'["x"]’ 
    Expected type: Expr '["x"] 
     Actual type: Expr (Remove "x" '["x"]) 
    In the expression: 
     (Lam (Proxy :: Proxy "x") (Var (Proxy :: Proxy "x"))) :: 
      Expr '["x"] 

---

j'ai changé les définitions donc il n'y a pas de dépendance bibliothèque singletons (plus facile à tester en ad hoc):

{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies, GADTs #-} 

import Data.Proxy 
import GHC.TypeLits 

type family Remove (x :: Symbol) (xs :: [Symbol]) where 
    Remove x '[] = '[] 
    Remove x (x ': xs) = Remove x xs 
    Remove x (y ': xs) = y ': Remove x xs 

data Expr (free :: [Symbol]) where 
    Var :: KnownSymbol a => Proxy a -> Expr '[a] 
    Lam :: KnownSymbol a => Proxy a -> Expr as -> Expr (Remove a as) 
-- App :: Expr free1 -> Expr free2 -> Expr (Union free1 free2)