我一直在试用bound包 - 你可以尝试使用的一个玩具示例是系统F.与包文档中的示例不同,它包含一个由lambda绑定的变量的类型参数,System F将有两个类型参数,一个用于普通变量(由普通的lambda抽象绑定),一个用于类型变量(由类型抽象绑定) .
我不太明白如何使用该软件包,但是看一下这些示例,我得到的印象是我应该首先为表达式类型编写一个 Monad
实例 . 然而,我遇到了麻烦,因为我无法想出一些类似于什么的东西,而且也是"obviously correct"(即通过检查看起来直观正确) . 到目前为止我有
{-# 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
设置monad实例?如果有,怎么样? -
Monad实例背后的直觉是什么?对于State / Maybe monad,我发现在扁平化(就连接而言)方面考虑是有用的 . 但是,我无法为Exp的Monad实例提出任何正确的直觉 . 绑定是否准确地进行捕获 - 避免替换?我读完这个post但是在普通的"De Bruijn indices"部分后迷路了 .