जीएचसी मेरे प्रकार के परिवार को क्यों नहीं कम करेगा?

Question

यहां एक अनियमित लैम्ब्डा कैलकुस है जिसका शब्द उनके मुक्त चर द्वारा अनुक्रमित किया गया है। मैं टाइप-स्तरीय तारों के सिंगलटन मानों के लिए singletons लाइब्रेरी का उपयोग कर रहा हूं।

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

ए Var एक नि: शुल्क चर प्रस्तुत करता है। एक लैम्ब्डा अमूर्तता एक चर को बांधती है जो शरीर में मुक्त दिखाई देती है (यदि कोई है जो मेल खाता है)। अनुप्रयोग अभिव्यक्ति के दो हिस्सों के मुक्त चरों में शामिल होते हैं, डुप्लिकेट को हटाते हैं (इसलिए x y के निशुल्क चर x और y हैं, जबकि x x के निशुल्क चर x हैं)।

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 

मैं इस इंटरैक्टिव प्रॉम्प्ट पर बाहर का परीक्षण किया:

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 

मैं जानने के लिए कि पहचान समारोह \x. x के प्रकार Expr (Remove "x" '["x"]), नहीं Expr '[] है हैरान था मैं उन प्रकार परिवारों बाहर लिखा था। जीएचसी प्रकार परिवार Remove का मूल्यांकन करने के इच्छुक नहीं है। मैं एक छोटे से अधिक प्रयोग किया और पता चला कि यह असल मेरी प्रकार परिवार के साथ एक समस्या नहीं है - GHC इस मामले में यह कम करने के लिए खुश है:

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

तो: क्यों नहीं GHC '[] लिए कम हो जाएगा Remove "x" '["x"] जब मैं मेरे जीएडीटी के प्रकार से पूछताछ करें? आम तौर पर, जब टाइपर टाइप प्रकार का प्रकार किसी प्रकार का परिवार मूल्यांकन करेगा? क्या ऐसे व्यवहार हैं जो मैं अपने व्यवहार से आश्चर्यचकित होने से बचने के लिए उपयोग कर सकता हूं?

Answer 1

यह काम करता है। जीएचसी सिर्फ आलसी लगता है।

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