Jaki jest właściwy sposób sprawdzania zgodności abstrakcji lambda za pomocą "bound"?

Question

Wdrażam prosty, zależnie pisany język, podobny do tego described by Lennart Augustsson, a także do zarządzania powiązaniami za pomocą bound.

Gdy typechecking zależną termin lambda, np λt:* . λx:t . x muszę:

1. "Enter" zewnętrzną spoiwo lambda, przy uruchamianiu t do coś
2. Typecheck λx:t . x, otrzymując ∀x:t . t
3. Pi-abstract the t, podając ∀t:* . ∀x:t . t

Jeśli lambda nie była zależna, mógłbym wykonać instancję t za pomocą jej typu w kroku 1, ponieważ typ jest wszystkim, co muszę wiedzieć o zmiennej podczas sprawdzania typu w kroku 2. Ale w kroku 3 brakuje mi informacje, aby zdecydować, które zmienne należy pominąć.

Mogę wprowadzić dostawę świeżej nazwy i utworzyć egzemplarz t z numerem Bound.Name.Name zawierającym typ i unikatową nazwę. Ale pomyślałem, że z bound nie powinienem generować nowych nazw.

Czy istnieje alternatywne rozwiązanie, którego mi brakuje?

Answer 1

Potrzebujemy jakiegoś kontekstu, aby śledzić argumenty lambda. Jednak niekoniecznie musimy je utworzyć, ponieważ bound podaje nam indeksy de Bruijna i możemy wykorzystać te indeksy do indeksowania w kontekście.

Faktycznie użycie indeksów jest jednak nieco zaangażowane ze względu na maszynę poziomu poziomu, która odzwierciedla rozmiar bieżącego zakresu (lub innymi słowy aktualną głębokość wyrażenia) poprzez zagnieżdżenie Var -s . Wymaga użycia polimorficznej rekursji lub GADT. Zapobiega to również przechowywaniu kontekstu w monadzie państwowej (ponieważ rozmiar, a tym samym rodzaj kontekstu zmienia się w miarę, jak się powtarzamy). Zastanawiam się jednak, czy moglibyśmy użyć monady z indeksem indeksowanym; byłby to zabawny eksperyment. Ale dygresję.

Najprostszym rozwiązaniem jest przedstawienie kontekstu jako funkcję:

type TC a = Either String a -- our checker monad 
type Cxt a = a -> TC (Type a) -- the context 

Wejście a zasadniczo wskaźnikiem de Bruijn i patrzymy się typ stosując funkcję indeksu. Możemy zdefiniować pustego kontekst następujący sposób:

emptyCxt :: Cxt a 
emptyCxt = const $ Left "variable not in scope" 

I możemy rozszerzyć kontekst:

consCxt :: Type a -> Cxt a -> Cxt (Var() a) 
consCxt ty cxt (B()) = pure (F <$> ty) 
consCxt ty cxt (F a) = (F <$>) <$> cxt a 

Wielkość kontekście jest kodowany w Var gniazdowania. Wzrost wielkości widoczny jest tutaj w typie zwrotu.

Teraz możemy napisać sprawdzanie typu. Główną kwestią jest to, że używamy fromScope i toScope, aby dostać się pod segregatory, a my przenosimy odpowiednio przedłużony Cxt (którego typ jest ustawiony idealnie).

data Term a 
    = Var a 
    | Star -- or alternatively, "Type", or "*" 
    | Lam (Type a) (Scope() Term a) 
    | Pi (Type a) (Scope() Term a) 
    | App (Type a) (Term a) 
    deriving (Show, Eq, Functor) 

-- boilerplate omitted (Monad, Applicative, Eq1, Show1 instances) 

-- reduce to normal form 
rnf :: Term a -> Term a 
rnf = ... 

-- Note: IIRC "Simply easy" and Augustsson's post reduces to whnf 
-- when type checking. I use here plain normal form, because it 
-- simplifies the presentation a bit and it also works fine. 

-- We rely on Bound's alpha equality here, and also on the fact 
-- that we keep types in normal form, so there's no need for 
-- additional reduction. 
check :: Eq a => Cxt a -> Type a -> Term a -> TC() 
check cxt want t = do 
    have <- infer cxt t 
    when (want /= have) $ Left "type mismatch" 

infer :: Eq a => Cxt a -> Term a -> TC (Type a) 
infer cxt = \case 
    Var a -> cxt a 
    Star -> pure Star -- "Type : Type" system for simplicity 
    Lam ty t -> do 
    check cxt Star ty 
    let ty' = rnf ty 
    Pi ty' . toScope <$> infer (consCxt ty' cxt) (fromScope t) 
    Pi ty t -> do 
    check cxt Star ty 
    check (consCxt (rnf ty) cxt) Star (fromScope t) 
    pure Star 
    App f x -> 
    infer cxt f >>= \case 
     Pi ty t -> do 
     check cxt ty x 
     pure $ rnf (instantiate1 x t) 
     _ -> Left "can't apply non-function" 

Oto the working code containing powyższe definicje. Mam nadzieję, że nie zepsułem tego zbyt mocno.