Substructural Polymorphism

Polymorphism.idr

import Data.Relevant.Cover as Rel
import Data.Linear.Cover as Lin

import Data.Vect

Ctx : Type
Ctx = List String

export infixr 5 ~>
data Ty : (typeVars : Ctx) -> Type where
  VarT : Ty [s]
  Forall : Ty (s::g) -> Ty g
  Mu : Ty (s::g) -> Ty g
  Imp : Rel.Cover k l m -> Ty k -> Ty l -> Ty m'

data TyEnv : Ctx -> Ctx -> Type where
  NilTy : TyEnv [] []
  ConsTy : (cov : Lin.Cover g1 g2 g) -> (tyEnv : TyEnv g1 d)
        -> (s : String) -> (ty : Ty g2) -> TyEnv g (s::d)

liftTy : TyEnv b a -> TyEnv (tyVar :: b) (tyVar :: a)

subTy : Ty g -> TyEnv d g -> Ty d

-- a trm is indexed by a list of type variables, and a list of term variables
data Term : (tyVars, trmVars : Ctx) -> Type where
  Var  : (var : String) -> Term tyVars [var]
  -- ^ a term variable is a singleton in some larger type context

  Lam  : (a : String) -> (tya : Ty tyVars)
      -> Term tyVars (a :: trmVars) -> Term tyVars trmVars

  App : Rel.Cover tyVars1 tyVars2 tyVars -> Rel.Cover trmVars1 trmVars2 trmVars
     -> Term tyVars1 trmVars1 -> Term tyVars2 trmVars2 -> Term tyVars trmVars

  In   : (f : Ty (tyVar :: tyVars)) -> Term tyVars trmVars -> Term tyVars trmVars
  Out  : (f : Ty (tyVar :: tyVars)) -> Term tyVars trmVars -> Term tyVars trmVars

  TLam : (tyVar : String) -> Ty (tyVar :: tyVars) -> Term (tyVar :: tyVars) trmVars -> Term tyVars trmVars

  TApp  : Rel.Cover tyVars1 tyVars2 tyVars -> Term tyVars1 trmVars -> Ty tyVars2 -> Term tyVars trmVars

namespace IxEnv
  -- This operation is not well-formed
  merge : Lin.Cover tyVars1 tyVars2 tyVars -> TyEnv tyVars1 tyVarsd -> TyEnv tyVars2 tyVarsd -> TyEnv tyVars tyVarsd
  merge Done NilTy NilTy = NilTy
  merge Done (ConsTy Done ty1 s z) (ConsTy Done ty2 s t) = ?nope --- <- we declared the same variable twice
  merge _ _ _ = ?xx

  data TrmEnv : (tyVarsg, trmVarsg, tyVarsd, trmVarsd : Ctx) -> TyEnv tyVarsg tyVarsd -> Type where
    NilTrm : TrmEnv [] [] [] [] NilTy
    ConsTrm : (cov : Lin.Cover tyVars1 tyVars2 tyVars) -> Lin.Cover trmVars1 trmVars2 trmVars
          -> TrmEnv tyVars1 trmVars1 tyVarsd trmVarsd sub1 -> (s : String) -> Term tyVars2 trmVars2
          -> (sub2 : TyEnv tyVars2 tyVarsd)
          -> TrmEnv tyVars trmVars tyVarsd (s::trmVarsd) (merge cov sub1 sub2)
                                                        -- ^ this is what we'd like to be true

    ConsTrmTy : (cov : Lin.Cover tyVars1 tyVars2 tyVars) -> TrmEnv tyVars1 trmVars1 tyVarsd trmVarsd sub1
              -> (s : String) -> (ty : Ty tyVars2)
              -> TrmEnv tyVars trmVars1 (s::tyVarsd) trmVarsd (ConsTy cov sub1 s ty)

--    AppendTrm : Lin.Cover tyVars1 tyVars2 tyVars -> Lin.Cover trmVars1 trmVars2 trmVars
--          -> Lin.Cover tyVars1d tyVars2d tyVarsd -> Lin.Cover trmVars1d trmVars2d trmVarsd
--          -> TrmEnv tyVars1 trmVars1 tyVars1d trmVars1d sub1
--          -> TrmEnv tyVars2 trmVars2 tyVars2d trmVars2d sub2
--          -> TrmEnv tyVars trmVars tyVarsd trmVarsd (?append' sub1 sub2)

  liftTrm : TyEnv tyd tyg -> TrmEnv tyd trmd tyg trmg env
         -> TrmEnv tyd (str :: trmd) tyg (str :: trmg) env

  liftTrmTy : TrmEnv tyd trmd tyg trmg env
          -> TrmEnv (tyVar :: tyd) trmd (tyVar :: tyg) trmg (liftTy env)

  subTerm : Term tyg trmg -> (sub1 : TyEnv tyd tyg) -> TrmEnv tyd trmd tyg trmg sub1 -> Term tyd trmd
  subTerm (Var var) env z = ?getVar
  subTerm (Lam str tya trm) env env1 = Lam str (subTy tya env) (subTerm trm env (liftTrm env env1))
  subTerm (App covty covtrm l r) env env1 = App ?cov' ?cov2' (subTerm l ?covty' ?covtrm') (subTerm r ?covty'' ?covtrm'')
  subTerm (In f x) env env1 = In (subTy f (liftTy env)) (subTerm x env env1)
  subTerm (Out f x) env env1 = Out (subTy f (liftTy env)) (subTerm x env env1)
  subTerm (TLam tyVar ty trm) env env1 = TLam tyVar (subTy ty (liftTy env)) (subTerm trm (liftTy env) (?lift' env1))
  subTerm (TApp c trm ty) env env1 = TApp ?c' (subTerm trm ?env' ?env1') (subTy ty ?env'')


namespace FibOp
  -- I think this should exist
  merge : Lin.Cover tyVars1 tyVars2 tyVars -> TyEnv tyVarsg tyVars1 -> TyEnv tyVarsg tyVars2 -> TyEnv tyVarsg tyVars

  -- TyEnv is now pointing in the opposite direction from TrmEnv!
  data TrmEnv : (tyVarsa, trmVarsg, tyVarsb, trmVarsd : Ctx) -> TyEnv tyVarsb tyVarsa -> Type where

  subTerm' : Term tyg trmg -> (sub1 : TyEnv tyg tyd) -> TrmEnv tyg trmd tyd trmg sub1 -> Term tyd trmd
  subTerm' t sub1 sub2 = ?subTerm'_rhs