Kappa calculus: the first-order fragment of typed lambda calculus

Kappa.hs

{-# LANGUAGE TupleSections #-}

module Kappa where

-- https://en.wikipedia.org/wiki/Kappa_calculus
-- https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=4854F9750FC1F1D658CC3694052C6A84?doi=10.1.1.53.715&rep=rep1&type=pdf
-- http://www.megacz.com/berkeley/garrows/megacz-pop-talk.pdf

import Control.Monad.Reader
import Safe

type Type = [()]

data Expr
  = Comp Expr Expr
  | Kappa Type Expr
  | Lift Type Expr
  | Var Int
  deriving Show

typeOf :: Expr -> ReaderT [Type] Maybe (Type, Type)
typeOf (Comp e1 e2) = do
  (s1, t1) <- typeOf e1
  (s2, t2) <- typeOf e2
  guard $ s1 == t2
  return (s2, t1)
typeOf (Kappa ty e) = do
  (s, t) <- local (ty:) $ typeOf e
  return (ty ++ s, t)
typeOf (Lift ty e) = do
  ([], t) <- typeOf e
  return (ty, t ++ ty)
typeOf (Var x) = do
  env <- ask
  lift $ ([],) <$> atMay env x

-- flip runReaderT [] . typeOf $ Kappa [] (Var 0)
-- flip runReaderT [] . typeOf $ Kappa [()] (Kappa [] (Var 0))
-- flip runReaderT [] . typeOf $ Kappa [()] (Comp (Lift [()] (Var 0)) (Var 0))