Typed.agda

open import Prelude

module Typed
  (Name   : Set)

  -- Data stuff
  (Datatype : Name -> List (List Name))

  -- Effect stuff
  (Effect : Set)
  (_⊆_    : Effect -> Effect -> Set)
  (Monad  : Effect -> Set -> Set)
  (return : forall {M A} -> A -> Monad M A)
  (map    : forall {M A B} -> (A -> B) -> Monad M A -> Monad M B)
  (join   : forall {M A} -> Monad M (Monad M A) -> Monad M A)
  (morph  : forall {M N} -> M ⊆ N -> (A : Set) -> Monad M A -> Monad N A)
  where

_=<<_ : forall {M A B} -> (A -> Monad M B) -> Monad M A -> Monad M B
k =<< m = join (map k m)

_>>=_ : forall {M A B} -> Monad M A -> (A -> Monad M B) -> Monad M B
m >>= k = k =<< m

infixl 50 _<*>_

_<*>_ : forall {M A B} -> Monad M (A -> B) -> Monad M A -> Monad M B
f <*> x = f >>= \f -> x >>= \x -> return (f x)

infixr 80 _⟶_
infix 100 [_]_

data VTy : Set

data CTy : Set where
  _⟶_  : VTy -> CTy -> CTy
  [_]_ : Effect -> VTy -> CTy

data VTy where
  ⟨_⟩   : CTy -> VTy
  TyCon : Name -> VTy

Cxt = List VTy

data ExC : Effect -> Cxt -> CTy -> Set
data InV : Effect -> Cxt -> VTy -> Set

data InC : Cxt -> CTy -> Set where

  ƛ_  : forall {V C Γ} ->
        InC (Γ ◄ V) C -> InC Γ (V ⟶ C)

  exC : forall {M N Γ V} ->
        ExC M Γ ([ N ] V) -> N ⊆ M -> InC Γ ([ M ] V)

  inV : forall {M Γ V} ->
        InV M Γ V -> InC Γ ([ M ] V)

InDs : Effect -> Cxt -> List Name -> Set

data InV where

  ⟪_⟫ : forall {M Γ C} -> InC Γ C -> InV M Γ ⟨ C ⟩

  ⟦_⟧ : forall {M Γ V} -> InC Γ ([ M ] V) -> InV M Γ V

  con : forall {M Γ D args} ->
        args ∈ Datatype D -> InDs M Γ args -> InV M Γ (TyCon D)

InDs M Γ = Box (\D -> InV M Γ (TyCon D))

data ExC where

  var : forall {M Γ V} -> V ∈ Γ -> ExC M Γ ([ M ] V)

  _•_ : forall {M Γ V C} ->
        ExC M Γ (V ⟶ C) -> InV M Γ V -> ExC M Γ C

Els : _

data El : Name -> Set where
  el : forall {args D} -> args ∈ Datatype D -> Els args -> El D

Els = Box El

VTy⟦_⟧ : VTy -> Set

CTy⟦_⟧ : CTy -> Set
CTy⟦ V ⟶ C   ⟧ = VTy⟦ V ⟧ -> CTy⟦ C ⟧
CTy⟦ [ M ] V ⟧ = Monad M VTy⟦ V ⟧


VTy⟦ ⟨ C ⟩   ⟧ = CTy⟦ C ⟧
VTy⟦ TyCon D ⟧ = El D

Env = Box VTy⟦_⟧

inC⟦_⟧ : forall {Γ C} -> InC Γ C -> Env Γ -> CTy⟦ C ⟧

inDs⟦_⟧ : forall {M Γ Ds} ->
          InDs M Γ Ds -> Env Γ -> Monad M (Els Ds)

inV⟦_⟧ : forall {M Γ V} -> InV M Γ V -> Env Γ -> Monad M VTy⟦ V ⟧
inV⟦ ⟪ c ⟫    ⟧ ρ = return (inC⟦ c ⟧ ρ)
inV⟦ ⟦ c ⟧    ⟧ ρ = inC⟦ c ⟧ ρ
inV⟦ con x Ds ⟧ ρ = return (el x) <*> inDs⟦ Ds ⟧ ρ

inDs⟦ ⟨⟩     ⟧ ρ = return ⟨⟩
inDs⟦ Ds ◃ v ⟧ ρ = return _◃_ <*> inDs⟦ Ds ⟧ ρ <*> inV⟦ v ⟧ ρ

exC⟦_⟧ : forall {M Γ C} -> ExC M Γ C -> Env Γ -> Monad M CTy⟦ C ⟧

inC⟦ ƛ c     ⟧ ρ = \v -> inC⟦ c ⟧ (ρ ◃ v)
inC⟦ exC c m ⟧ ρ = morph m _ =<< exC⟦ c ⟧ ρ
inC⟦ inV v   ⟧ ρ = inV⟦ v ⟧ ρ

exC⟦ var x ⟧ ρ = return (return (ρ ! x))
exC⟦ f • s ⟧ ρ = exC⟦ f ⟧ ρ <*> inV⟦ s ⟧ ρ