2015-07-16 31 views
6

Şartları serbest değişkenleri tarafından endekslenen bir türlenmemiş lambda hesabı. Tür düzeyinde dizeleri tekil değerler için singletons kitaplığı kullanıyorum. Var, bir serbest değişken sunar. Bir lambda soyutlaması, vücutta serbest olan bir değişkeni (eşleşen bir tane varsa) bağlar. Uygulamalar ifadenin iki bölümünün serbest değişkenlerini birleştirerek, kopyaları kaldırarak (x y serbest değişkenleri x ve y, x x serbest değişkenleri ise yalnızca x). Ben interaktif isteminde bu testGHC neden tip ailemi azaltmıyor?

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 

Ben kimlik işlevi \x. x tipi Expr (Remove "x" '["x"]) değil Expr '[] olduğunu öğrenmek için sürpriz oldu O tip aileleri yazdım. GHC, Remove aile tipini değerlendirmek istemiyor gibi görünüyor. Ben biraz daha tecrübe ve se başına benim tipim ailesi ile ilgili bir sorun olmadığını öğrendik - GHC bu durumda bunu azaltmak için mutludur:

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

Yani: Neden olmasın GHC '[] için Remove "x" '["x"] azaltacaktır zaman GADT’imin türünü sorgula? Genel olarak, tip denetçisi ne zaman bir tür aile değerlendirirse değerlendirmez? Davranışından şaşmamak için kullanabileceğim buluşsal yöntemler var mı?

+4

“Neden GHC ailemi azaltmaz: singletons kütüphanede orada bağımlılık değildir bu yüzden

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

Ben tanımları değişti (daha kolay, anlık test etmek)? ”Ve çok acımasız geliyordu. –

+1

@JoachimBreitner En iyi derleyiciler bile, –

+1

olmasını istediğiniz her şeyi yapamazlar. Https://wiki.haskell.org/GHC/Type_families#Closed_family_simplification adresindeki “Remove” öğesindeki örtüşen tanımlardan şüphelenirim. Muhtemelen bir tür kısıtlamaya gereksiniminiz vardır, bu türlerin eşitsiz olduğuna inanıyoruz – phadej

cevap

2

Çalışıyor. GHC sadece tembel görünüyor.

Okuduğum
{-# 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) 
+0

Yani "Kaldır" x "'[" x "]' '[[]' ile birleşir, ancak normalleştirmez, en azından şu anda interaktif bilgi istemi Bir fikrin neden? "GHC sadece tembel görünüyor" kesinlikle doğru, ama daha aydınlatıcı bir açıklama umuyordum! –

+0

% 100 emin değilim. https://wiki.haskell.org/GHC/Type_families#Closed_family_simplification, GADT'lerin işleri nasıl zorlaştırdığı hakkında bir bölüm var. Yani belki de * tembel *, ama * dikkatli * (birisinin aynı anlayabileceği :)). – phadej