使用带有多个类型变量的绑定进行抽象

我一直在尝试 bound package-您可以尝试使用的一个玩具示例是system f。与package文档中的示例不同,其中一个类型参数用于被lambda绑定的变量,system f将有两个类型参数,一个用于普通变量(由普通lambda抽象绑定),另一个用于类型变量(由类型抽象绑定)。

我不太明白如何使用这个包,但是看看这些例子,我觉得我应该从写一个 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)

1. 有没有可能有一个Monad实例 Exp t ?如果是,怎么办?
2. Monad实例背后的直觉是什么?对于状态/可能是单子,我发现将它们视为链接计算(在绑定方面)很有用,而对于列表之类的结构,我发现将它们视为扁平计算(在连接方面)很有用。然而,对于exp的monad实例,我无法给出任何正确的直觉。bind是否精确地做到捕获避免替换?我通读过这个 post 但在普通的“de bruijn指数”部分之后就迷路了。