Я хотел бы расширить отличный ответ @Daniel Wagner с немного другим подходом: вместо проверки типов, возвращающей допустимый тип (если он есть), возвращайте типизированное выражение, которое затем гарантирует, что мы можем его оценить (поскольку просто типизированная лямбда исчисление сильно нормализует). Основная идея состоит в том, что check ctx t e
возвращает Just (ctx |- e :: t)
тогда и только тогда, когда e
может быть введено в t
в некотором контексте ctx
, а затем, имея некоторое типизированное выражение ctx |- e :: t
, мы можем оценить его в некотором Env
железе правильного типа.
Реализация
Я буду использовать синглтоны для эмуляции типа Pi check :: (ctx :: [Type]) -> (a :: Type) -> Term -> Maybe (TTerm ctx a)
, что означает, что нам нужно будет включить каждое расширение GHC и кухонную раковину:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
{-# LANGUAGE TemplateHaskell #-} -- sigh...
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Type.Equality
Первый бит - это нетипизированное представление, прямо из ответа @Daniel Wagner:
data Type = Base
| Arrow Type Type
deriving (Show, Eq)
data Term = Const
| Var Int
| Lam Type Term
| App Term Term
deriving Show
но мы также дадим семантику для этих типов, интерпретируя Base
как ()
и Arrow t1 t2
как t1 -> t2
:
type family Interp (t :: Type) where
Interp Base = ()
Interp (Arrow t1 t2) = Interp t1 -> Interp t2
Продолжая тему де Брейна, контексты — это список типов, а переменные — это индексы контекста. Учитывая среду типа контекста, мы можем найти индекс переменной, чтобы получить значение. Обратите внимание, что lookupVar
— это суммарная функция.
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
Итак, у нас есть вся инфраструктура для написания кода. Прежде всего, давайте определим типизированное представление Term
вместе с (всего!) оценщиком:
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
Все идет нормально. eval
удобен и тотален, потому что его входные данные могут представлять только хорошо типизированные термины простого лямбда-исчисления. Таким образом, часть работы оценщика @Daniel должна быть выполнена по преобразованию нетипизированного представления в типизированное.
Основная идея infer
заключается в том, что если вывод типа выполнен успешно, он возвращает Just $ TheTerm t e
, где t
— это Sing
leton-свидетель типа e
.
$(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
Надеюсь, что последний шаг очевиден: поскольку мы можем оценить правильно типизированный терм только для заданного типа (поскольку именно это дает нам тип его внедрения в Haskell), мы превращаем тип infer
ence в тип 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'
Пример сеанса
Давайте попробуем наши функции в 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' () ()
()
person
Cactus
schedule
08.01.2015
()
, кортежи(,)
и лямбда-конструктор для функций — он пытается вывести объект с заданным типом. Есть вопрос, связанный с a> о выводе кода Haskell из типов. - person Cirdec   schedule 08.01.2015s
, кажется, указывает на то, что вам нужна динамическая проверка, но вы должны уточнить это. - person chi   schedule 08.01.2015