Я пробовал пакет bound - один из игрушечных примеров, с которым вы можете попробовать это, - System F. В отличие от примеров в документации пакета, в которых есть один параметр типа для переменной, связанной слямбда, система F будет иметь два параметра типа, один для обычных переменных (связанных обычной лямбда-абстракцией) и один для переменных типа (связанных абстракциями типов).
Я не совсем понимаю, как использоватьпакет, но, глядя на примеры, у меня сложилось впечатление, что я должен начать с написания Monad экземпляра для типа выражения.Тем не менее, я столкнулся с проблемой, так как я не могу придумать что-то, что проверяет тип, а также является «явно правильным» (то есть, кажется, что оно интуитивно верно проверяется).Пока у меня есть
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}
module SystemF where
import Bound
import Control.Monad
import Data.Bifunctor
-- e ::= x | λx : τ. e | e1 e2 | ΛX. e | e [τ]
-- t denotes type variables, e denotes expression variables
data Exp t e
= Var e
| Lam (Scope () (Exp t) e)
| App (Exp t e) (Exp t e)
| TyLam (Scope () (FlipExp e) t) -- Is this correct?
| TyApp (Exp t e) (Type t)
newtype FlipExp e t = FlipExp { getExp :: Exp t e }
instance Functor (Exp t) where
fmap = second
instance Bifunctor Exp where
bimap f g = \case
Var e -> Var (g e)
Lam s -> Lam (bimapInScope f g s)
App e1 e2 -> App (bimap f g e1) (bimap f g e2)
TyLam s' -> TyLam (bimapInScope g f s')
TyApp e t -> TyApp (bimap f g e) (fmap f t)
where
bimapInScope f g = Scope . bimap f (second (bimap f g)) . unscope
instance Applicative (Exp t) where
pure = Var
(<*>) = ap
instance Monad (Exp t) where
x >>= f = case x of
Var v -> f v
Lam s -> Lam (s >>>= f)
App e1 e2 -> App (e1 >>= f) (e2 >>= f)
TyLam s ->
-- tmp :: Exp (Var () (Exp t a) a
-- but we need Exp (Var () (Exp t b)) b
-- just applying >>= inside the first argument
-- is insufficient as the outer 'a' won't change
let tmp = first (second getExp) $ getExp (unscope s)
in error "How do I implement this?"
TyApp e t -> TyApp (e >>= f) t
instance Functor (FlipExp e) where
fmap = second
instance Bifunctor FlipExp where
bimap f g = FlipExp . bimap g f . getExp
-- τ ::= X | τ -> τ | ∀ X . τ
data Type t
= TVar t
| TFun (Type t) (Type t)
| TForall (Scope () Type t)
deriving (Functor, Foldable, Traversable)
instance Applicative Type where
pure = TVar
(<*>) = ap
instance Monad Type where
x >>= f = case x of
TVar v -> f v
TFun t1 t2 -> TFun (t1 >>= f) (t2 >>= f)
TForall s -> TForall (s >>>= f)
- Можно ли иметь экземпляр монады для
Exp t?Если да, то как? - Какова интуиция за экземпляром Монады?Что касается монад State / Maybe, я считаю полезным думать о них как о цепочечных вычислениях (с точки зрения связывания), тогда как для таких структур, как списки, я считаю полезным думать с точки зрения выравнивания (с точки зрения объединения).).Однако я не могу придумать какую-либо правильную интуицию для экземпляра Monad для Exp.Связывает ли точно замену, избегающую захвата?Я прочитал этот пост , но затерялся после обычного раздела «Индексы де Брюйна».