Abbiamo bisogno di un qualche tipo di contesto per tenere traccia degli argomenti lambda. Tuttavia, non abbiamo necessariamente bisogno di istanziarli, dal momento che bound ci fornisce gli indici de Bruijn e possiamo usare quegli indici per indicizzare nel contesto.
In realtà l'utilizzo degli indici è un po 'complicato, tuttavia, a causa del macchinario di livello del tipo che riflette le dimensioni dell'ambito corrente (o in altre parole, la profondità corrente nell'espressione) attraverso l'annidamento di Var -s . Richiede l'uso della ricorsione polimorfica o GADT. Ci impedisce anche di memorizzare il contesto in una monade di stato (perché le dimensioni e quindi il tipo di contesto cambiano mentre ricorrono). Mi chiedo però se potessimo usare una monade indicizzata di stato; sarebbe un esperimento divertente. Ma sto divagando.
La soluzione più semplice è quello di rappresentare il contesto in funzione:
type TC a = Either String a -- our checker monad
type Cxt a = a -> TC (Type a) -- the context
L'ingresso a è essenzialmente un indice de Bruijn, e cercare un tipo applicando la funzione all'indice. Possiamo definire il contesto vuoto seguente modo:
emptyCxt :: Cxt a
emptyCxt = const $ Left "variable not in scope"
E possiamo estendere contesto:
consCxt :: Type a -> Cxt a -> Cxt (Var() a)
consCxt ty cxt (B()) = pure (F <$> ty)
consCxt ty cxt (F a) = (F <$>) <$> cxt a
La dimensione del contesto è codificato nel Var nesting. L'aumento delle dimensioni è evidente qui nel tipo di ritorno.
Ora possiamo scrivere il controllo di tipo. Il punto principale qui è che usiamo fromScope e toScope per ottenere sotto leganti, e portiamo avanti uno Cxt opportunamente esteso (il cui tipo si allinea perfettamente).
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"
Ecco le definizioni di cui sopra the working code containing. Spero di non averlo incasinato troppo.
Qualunque cosa tu faccia, dovrai mantenere la distinzione di t. Ciò è necessario se stai facendo l'astrazione Pi (come ti astraggerebbe se non puoi vederlo distintamente?), Ma è anche necessario digitare il corpo (t è un tipo, diverso da molti altri tipi). Puoi tenere t de Bruijn, ma poi devi essere un po 'più attento a come lavorare con il suo raccoglitore. Prenderò un nuovo nome, e in effetti metterei in cache il tipo con esso. Sono interessato a vedere approcci alternativi. – pigworker