Po prostu wpisano rachunek lambda z niepowodzeniem, w Haskell

Question

Jestem nowym użytkownikiem Haskell, więc przepraszam, jeśli to pytanie nie ma zbytniego sensu.

Chcę móc zaimplementować po prostu wpisane wyrazy lambda w Haskell w taki sposób, że gdy próbuję zastosować wyrażenie do innego typu niewłaściwy, wynik nie jest błędem typu, ale raczej zestaw wartość, np Nic. Na początku myślałem, że użycie Monady Być może będzie właściwym podejściem, ale nie udało mi się uzyskać niczego działającego. Zastanawiałem się, co, jeśli w ogóle, byłby to właściwy sposób.

Kontekst problemu, jeśli pomaga, to projekt, nad którym pracuję, który przypisuje znaczniki POS (część mowy) do słów w zdaniach. W przypadku zestawu tagów używam typów gramatyki kategorii; są to wyrazy typu lambda, takie jak (e -> s) lub (e -> (e -> s)), gdzie e i s są typami odpowiednio dla rzeczowników i zdań. Na przykład kill ma typ (e -> (e -> s)) - wymaga dwóch zdań rzeczownikowych i zwraca zdanie. Chcę napisać funkcję, która pobiera listę obiektów tego typu i dowiaduje się, czy istnieje jakiś sposób połączenia ich w celu osiągnięcia obiektu typu s. Oczywiście, właśnie to sprawdza Haskell, więc powinno być proste przyporządkowanie każdego słowa wyrażenia lambda odpowiedniego typu i pozwolić Haskellowi zrobić resztę. Problem polega na tym, że jeśli nie można uzyskać dostępu do s, program sprawdzający typ Haskella naturalnie przerywa działanie programu.

Answer 1

Całkiem standardowe rzeczy. Po prostu napisz sprawdzanie typu i oceniaj tylko termin, gdy sprawdza on typologię. evalMay to robi. Możesz oczywiście wzbogacić zbiór stałych i typów podstawowych; Po prostu użyłem jednego dla uproszczenia.

import Control.Applicative ((<$), (<$>)) 
import Control.Monad (guard) 
import Safe (atMay) 

data Type 
    = Base 
    | Arrow Type Type 
    deriving (Eq, Ord, Read, Show) 

data Term 
    = Const 
    | Var Int -- deBruijn indexing; the nearest enclosing lambda binds Var 0 
    | Lam Type Term 
    | App Term Term 
    deriving (Eq, Ord, Read, Show) 

check :: [Type] -> Term -> Maybe Type 
check env Const = return Base 
check env (Var v) = atMay env v 
check env (Lam ty tm) = Arrow ty <$> check (ty:env) tm 
check env (App tm tm') = do 
    Arrow i o <- check env tm 
    i' <- check env tm' 
    guard (i == i') 
    return o 

eval :: Term -> Term 
eval (App tm tm') = case eval tm of 
    Lam _ body -> eval (subst 0 tm' body) 
eval v = v 

subst :: Int -> Term -> Term -> Term 
subst n tm Const = Const 
subst n tm (Var m) = case compare m n of 
    LT -> Var m 
    EQ -> tm 
    GT -> Var (m-1) 
subst n tm (Lam ty body) = Lam ty (subst (n+1) tm body) 
subst n tm (App tm' tm'') = App (subst n tm tm') (subst n tm tm'') 

evalMay :: Term -> Maybe Term 
evalMay tm = eval tm <$ check [] tm 

Answer 2

Chciałbym przedłużyć doskonałą odpowiedź @Daniel Wagnera z nieco innego podejścia: zamiast typechecking powracającego poprawny typ (jeśli istnieje), zwracają wpisane wyrażenie, które jest następnie gwarantowaną możemy go ocenić (ponieważ prosty rachunek lambda jest silnie normalizowany). Podstawowym założeniem jest to, że check ctx t e powraca Just (ctx |- e :: t) IFF e może być wpisany na t w jakimś kontekście ctx, a następnie podane jakieś wpisane wyrażenie ctx |- e :: t możemy ocenić go w jakiś Env ironment prawego typu.

Realizacja

będę używał pojedynczych emulować typ PI check :: (ctx :: [Type]) -> (a :: Type) -> Term -> Maybe (TTerm ctx a), co oznacza, że ​​musimy włączyć każdego rozszerzenia GHC i zlewozmywaka:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-} 
{-# LANGUAGE TemplateHaskell #-} -- sigh... 

import Data.Singletons.Prelude 
import Data.Singletons.TH 
import Data.Type.Equality 

Pierwszy bit jest bez typu reprezentacja, prosto z odpowiedzią @Daniel Wagnera:

data Type = Base 
      | Arrow Type Type 
      deriving (Show, Eq) 

data Term = Const 
      | Var Int 
      | Lam Type Term 
      | App Term Term 
      deriving Show 

ale będziemy też dać semantykę dla tych typów interpretując Base jak () i Arrow t1 t2 jak t1 -> t2:

type family Interp (t :: Type) where 
    Interp Base =() 
    Interp (Arrow t1 t2) = Interp t1 -> Interp t2 

Aby zachować z tematem de Bruijn, konteksty są wykaz rodzajów i zmienne są wskaźniki kontekstu. Biorąc pod uwagę środowisko typu kontekstowego, możemy wyszukać indeks zmienny, aby uzyskać wartość. Zauważ, że lookupVar jest funkcją całkowitą.

data VarIdx (ts :: [Type]) (a :: Type) where 
    Here :: VarIdx (a ': ts) a 
    There :: VarIdx ts a -> VarIdx (b ': ts) a 

data Env (ts :: [Type]) where 
    Nil :: Env '[] 
    Cons :: Interp a -> Env ts -> Env (a ': ts) 

lookupVar :: VarIdx ts a -> Env ts -> Interp a 
lookupVar Here  (Cons x _) = x 
lookupVar (There v) (Cons _ xs) = lookupVar v xs 

OK, mamy całą infrastrukturę, aby napisać kod. Przede wszystkim, niech określić wpisane reprezentację Term wraz z (całkowita!) Oceniającego:

data TTerm (ctx :: [Type]) (a :: Type) where 
    TConst :: TTerm ctx Base 
    TVar :: VarIdx ctx a -> TTerm ctx a 
    TLam :: TTerm (a ': ctx) b -> TTerm ctx (Arrow a b) 
    TApp :: TTerm ctx (Arrow a b) -> TTerm ctx a -> TTerm ctx b 

eval :: Env ctx -> TTerm ctx a -> Interp a 
eval env TConst =() 
eval env (TVar v) = lookupVar v env 
eval env (TLam lam) = \x -> eval (Cons x env) lam 
eval env (TApp f e) = eval env f $ eval env e 

tej pory tak dobrze. eval jest niezły, ponieważ jego dane wejściowe mogą reprezentować tylko dobrze napisane terminy zwykłego rachunku lambda. Więc część pracy z ewaluatora @ Daniela będzie musiała zostać wykonana w transformacji reprezentacji bez typu na typową.

Podstawową ideą jest to, że jeśli infer wnioskowanie typu powiedzie, zwraca Just $ TheTerm t e, gdzie t jest świadkiem Sing leton typu e „s.

$(genSingletons [''Type]) 
$(singDecideInstance ''Type) 

-- I wish I had sigma types... 
data SomeTerm (ctx :: [Type]) where 
    TheTerm :: Sing a -> TTerm ctx a -> SomeTerm ctx 

data SomeVar (ctx :: [Type]) where 
    TheVar :: Sing a -> VarIdx ctx a -> SomeVar ctx 

-- ... and pi ones as well 
infer :: Sing ctx -> Term -> Maybe (SomeTerm ctx) 
infer _ Const = return $ TheTerm SBase TConst 
infer ts (Var n) = do 
    TheVar t v <- inferVar ts n 
    return $ TheTerm t $ TVar v 
infer ts (App f e) = do 
    TheTerm t0 e' <- infer ts e 
    TheTerm (SArrow t0' t) f' <- infer ts f 
    Refl <- testEquality t0' t0 
    return $ TheTerm t $ TApp f' e' 
infer ts (Lam ty e) = case toSing ty of 
    SomeSing t0 -> do 
     TheTerm t e' <- infer (SCons t0 ts) e 
     return $ TheTerm (SArrow t0 t) $ TLam e' 

inferVar :: Sing ctx -> Int -> Maybe (SomeVar ctx) 
inferVar (SCons t _) 0 = return $ TheVar t Here 
inferVar (SCons _ ts) n = do 
    TheVar t v <- inferVar ts (n-1) 
    return $ TheVar t $ There v 
inferVar _ _ = Nothing 

Mam nadzieję, że ostatni krok jest oczywista: ponieważ możemy tylko ocenić dobrze wpisany termin w danym typie (ponieważ to właśnie daje nam rodzaj jego Haskell osadzania), zwracamy type infer ence w rodzaju check ing:

check :: Sing ctx -> Sing a -> Term -> Maybe (TTerm ctx a) 
check ctx t e = do 
    TheTerm t' e' <- infer ctx e 
    Refl <- testEquality t t' 
    return e' 

Przykład sesji

Spróbujmy nasze funkcje w GHCi:

λ» :set -XStandaloneDeriving -XGADTs 
λ» deriving instance Show (VarIdx ctx a) 
λ» deriving instance Show (TTerm ctx a) 

λ» let id = Lam Base (Var 0) -- \x -> x 
λ» check SNil (SBase `SArrow` SBase) id 
Just (TLam (TVar Here)) 

λ» let const = Lam Base $ Lam Base $ Var 1 -- \x y -> x 
λ» check SNil (SBase `SArrow` SBase) const 
Nothing -- Oops, wrong type 
λ» check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const 
Just (TLam (TLam (TVar Here))) 

λ» :t eval Nil <$> check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const 
eval Nil <$> check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const 
    :: Maybe (() ->() ->()) 
-- Note that the `Maybe` there comes from `check`, not `eval`! 
λ» let Just const' = check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const 
λ» :t eval Nil const' 
eval Nil const' ::() ->() ->() 
λ» eval Nil const'()() 
()