Using Bound with multiple type variables for abstractions

Question

I've been trying out the bound package - one toy example you can try this with is System F. Unlike the examples in the package documentation which have one type parameter for the variable being bound by a lambda, System F will have two type parameters, one for ordinary variables (bound by an ordinary lambda abstraction) and one for type variables (bound by type abstractions).

I don't quite understand how to use the package, but looking at the examples, the impression I get is that I should start with writing a Monad instance for an expression type. However, I ran into trouble, as I am not able to come up with something that typechecks and is also "obviously correct" (i.e. seems intuitively correct by inspection). So far I have

{-# 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. Is it possible to have a monad instance for Exp t? If yes, how?
2. What is the intuition behind the Monad instance? For the State/Maybe monads, I've found it useful to think of them as chaining computations (in terms of bind), whereas for structures like Lists, I've found it useful to think in terms of flattening (in terms of join). However, I am unable to come up with any proper intuition for the Monad instance for Exp. Does bind precisely do capture-avoiding substitution? I read through this post but got lost after the ordinary "De Bruijn indices" section.

Answer 1

See the discussion here and @phadej's bound-extras package here.

The gist is that type abstraction is a term-level thing (so a variant of Expr) that needs to abstract over Types. Plain Scope b f a is unsuited to deal with this, as its expansion f (Either b (f a)) has f fixed for both occurrences. You want the outer f be an Expr, while the inner should be a Type. That leads to the following generalisations of Scope:

newtype ScopeH b f g a = ScopeH (g (Either b (f a)))
newtype ScopeT b t f a = ScopeT (t f (Either b (f a)))

newtype Expr' a b = Expr' (Expr b a)
data Expr b a
  = V a
  ...
  | TyApp (Expr b a) (Ty b)
  | Forall (ScopeH () (Expr' a) Ty b)
  ...

Expr' a fixes the de Bruijn index for term vars, so that the ScopeH constructor can introduce an additional type var to be put in b holes.