Perché GHC non ridurrà la mia famiglia di tipi?

Question

Ecco un calcolo lambda non tipizzato i cui termini sono indicizzati dalle loro variabili libere. Sto usando la libreria singletons per i valori singleton delle stringhe a livello di testo.

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE UndecidableInstances #-} 

import Data.Singletons 
import Data.Singletons.TypeLits 

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

A Var introduce una variabile libera. Un'astrazione lambda lega una variabile che appare libera nel corpo (se ce n'è una che corrisponde). Le applicazioni uniscono le variabili libere delle due parti dell'espressione, rimuovendo i duplicati (quindi le variabili libere di x y sono x e , mentre le variabili libere di x x sono solo x). Ho scritto quelle famiglie tipo:

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 

ho provato questo fuori al prompt interattivo:

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 

Sono rimasto sorpreso di apprendere che il tipo di funzione identità \x. x è Expr (Remove "x" '["x"]), non Expr '[]. GHC sembra riluttante a valutare la famiglia di tipi Remove. Ho sperimentato un po 'di più e ho imparato che non è un problema con il mio tipo familiare per sé - GHC è felice di ridurla in questo caso:

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

Quindi: Perché non il GHC ridurre Remove "x" '["x"] a '[] quando ho interrogare il tipo del mio GADT? In generale, quando testamento di tipo non sarà valutato da una famiglia di tipi? Ci sono euristiche che posso usare per evitare di essere sorpreso dal suo comportamento?

Answer 1

Funziona. GHC sembra essere solo pigro.

λ *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"] 

---

ho cambiato le definizioni in modo non v'è dipendenza da biblioteca single (più facile da testare in 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)