Polarised System L

1_Ty.idr

module Ty

public export
data Kind : Type where
  Set : Kind
  Op : Kind

public export
data Dual : Kind -> Kind -> Type where
  L : Dual Set Op
  R : Dual Op Set

public export
data Ty : Kind -> Type where
  Zero : Ty k
  Add : Ty k -> Ty k -> Ty k
  One : Ty k
  Mult : Ty k -> Ty k -> Ty k
  Not : Dual c op -> Ty c -> Ty op
  Shift : Dual c op -> Ty c -> Ty op

public export
NotN : Ty Op -> Ty Set
NotN = Not R

public export
NotP : Ty Set -> Ty Op
NotP = Not L

public export
Down : Ty Op -> Ty Set
Down = Shift R

public export
Up : Ty Set -> Ty Op
Up = Shift L

public export
Ten : Ty Set -> Ty Set -> Ty Set
Ten = Mult

public export
Sum : Ty Set -> Ty Set -> Ty Set
Sum = Add

public export
Par : Ty Op -> Ty Op -> Ty Op
Par = Mult

public export
With : Ty Op -> Ty Op -> Ty Op
With = Add

public export
--a -> b == (¬a) par b
Imp : Ty Set -> Ty Op -> Ty Op
Imp a b = Par (NotP a) b

2_Term.idr

module Term
import Ty

export infixr 5 ~>

public export
data Ctx : Type where
  Nil : Ctx
  (::) : {k : Kind} -> Ty k -> Ctx -> Ctx

public export
data Elem : (k : Kind) -> Ty k -> Ctx -> Type where
  Here  : Elem k x (x :: xs)
  There : Elem k x ys -> Elem k x (y::ys)

mutual
  public export
  -- +ve and -ve Commands are indexed by a kind
  data Cmd : Ctx -> Kind -> Ctx -> Type where
    CPos : {a : Ty Set} -> TermP g a d   -> CoTermP g a d -> Cmd g Set d
    CNeg : {a : Ty Op}  -> CoTermN g a d -> TermN g a d -> Cmd g Op d

  -- +ve terms
  public export
  data TermP : Ctx -> Ty Set -> Ctx -> Type where
    MuP : Cmd g Set (a::d) -> TermP g a d
    Val : Value g a d       -> TermP g a d

  -- -ve coterms
  public export
  data CoTermN : Ctx -> Ty Op -> Ctx -> Type where
    MutN   : Cmd (a::g) Op d              -> CoTermN g a d
    CoVal  : Stack g a d                  -> CoTermN g a d

  -- +ve Values
  public export
  data Value : Ctx -> Ty Set -> Ctx -> Type where
    VarP  : Elem Set a g -> Value g a d
    Pair  : {a, b : Ty Set} -> Value g a d -> Value g b d -> Value g (Ten a b) d
    Inl   : {x, y : Ty Set} -> Value g x d -> Value g (Sum x y) d
    Inr   : {x, y : Ty Set} -> Value g y d -> Value g (Sum x y) d
    Init  : Value g One d
    NotNR : {e : Ty Op} -> Stack g e d -> Value g (NotN e) d
    DownR : {e : Ty Op} -> TermN g e d -> Value g (Down e) d

  -- -ve Values
  public export
  data Stack : Ctx -> Ty Op -> Ctx -> Type where
    VarN   : Elem Op a d -> Stack g a d
    Empty  : Stack g a d
    Fst    : {a : Ty Op} -> Stack g a d -> Stack g (With a b) d
    Snd    : {b : Ty Op} -> Stack g b d -> Stack g (With a b) d
    Para   : {a, b : Ty Op} -> Stack g a d -> Stack g b d -> Stack g (Par a b) d
    True  : Stack g One d
    NotPL : {e : Ty Set} -> Value g e d -> Stack g (NotP e) d
    UpL   : {e : Ty Set} -> CoTermP g e d -> Stack g (Up e) d

  -- +ve coterms
  public export
  data CoTermP : Ctx -> Ty Set -> Ctx -> Type where
    CoVarP : Elem Set a d -> CoTermP g a d
    EmptyP : CoTermP g a d
    MutP : Cmd (a::g) Set d -> CoTermP g a d
    MatchPair : {x, y : Ty Set} -> Cmd (x::y::g) Set d -> CoTermP g (Ten x y) d
    Case : {x, y : Ty Set} -> Cmd (x::g) Set d -> Cmd (y::g) Set d -> CoTermP g (Sum x y) d
    MatchNegL : {a : Ty Op} -> Cmd g Set (a::d) -> CoTermP g (NotN a) d
    MatchDown : {a : Ty Op} -> Cmd (a::g) Set d -> CoTermP g (Down a) d

  -- -ve terms
  data TermN : Ctx -> Ty Op -> Ctx -> Type where
    CoVarN : {a : Ty Op} -> Elem Op a g -> TermN g a d
    MuN : {a : Ty Op} -> Cmd g Op (a::d) -> TermN g a d
    CoCase : {a, b : Ty Op} -> Cmd g Op (a::d)
           -> Cmd g Op (b::d) -> TermN g (With a b) d
    CoMatchPar : {a, b : Ty Op} -> Cmd g Op (a::b::d) -> TermN g (Par a b) d
    CoMatchNegR : {a : Ty Set} -> Cmd (a::g) Op d -> TermN g (NotP a) d
    CoMatchUp : {a : Ty Set}   -> Cmd g Op (a::d) -> TermN g (Up a) d

3_Reduce.idr

subst1P : {g, d : Ctx} -> {a : Ty Set} -> Cmd (a :: g) k d -> Value g a d -> Cmd g k d

cosubst1N : {g, d : Ctx} -> {a : Ty Op} -> Cmd (a :: g) k d -> TermN g a d -> Cmd g k d

cosubst1P : {g, d : Ctx} -> {a : Ty Set} -> Cmd g k (a :: d) -> CoTermP g a d -> Cmd g k d

subst1N   : {g, d : Ctx} -> {a : Ty Op} -> Cmd g k (a :: d) -> Stack g a d -> Cmd g k d

subst2P : {g, d : Ctx} -> {a, b : Ty Set}
       -> Cmd (a :: (b :: g)) k d -> Value g a d -> Value g b d -> Cmd g k d

subst2N :  {g, d : Ctx} -> {a, b : Ty Op}
       -> Cmd g k (a :: b :: d) -> Stack g a d -> Stack g b d -> Cmd g k d

reduce : {g, d : Ctx} -> Cmd g k d -> Maybe (Cmd g k d)
reduce (CPos (MuP c) e)                    = Just $ cosubst1P c e
reduce (CPos (Val v) (MutP c))             = Just $ subst1P c v
reduce (CPos (Val (Pair t u)) (MatchPair c))    = Just $ subst2P c t u
reduce (CPos (Val (Inl v)) (Case l _))     = Just $ subst1P l v
reduce (CPos (Val (Inr v)) (Case _ r))     = Just $ subst1P r v
reduce (CPos (Val (NotNR s)) (MatchNegL c))  = Just $ subst1N c s
reduce (CPos (Val (DownR t)) (MatchDown c))  = Just $ cosubst1N c t
reduce (CNeg (MutN c) t)                 = Just $ cosubst1N c t
reduce (CNeg (CoVal s) (MuN c))          = Just $ subst1N c s
reduce (CNeg (CoVal (Fst s)) (CoCase l _)) = Just $ subst1N l s
reduce (CNeg (CoVal (Snd s)) (CoCase _ r)) = Just $ subst1N r s
reduce (CNeg (CoVal (Para l r)) (CoMatchPar c)) = Just $ subst2N c l r
reduce (CNeg (CoVal (NotPL s)) (CoMatchNegR c)) = Just $ subst1P c s
reduce (CNeg (CoVal (UpL s)) (CoMatchUp c))  = Just $ cosubst1P c s

4_Examples.idr

-- Positive identity
posId : {a : Ty Set} -> Cmd [a] Set [a]
posId = CPos (Val $ VarP Here) (CoVarP Here)

-- Injection into a strict sum
posInL : {a, b : Ty Set} -> Cmd [a] Set [Sum a b]
posInL = CPos (Val $ Inl $ VarP Here) (CoVarP Here)

-- Projection from a lazy product
negFst :  {a, b : Ty Op} -> Cmd [With a b] Op [a]
negFst = CNeg (CoVal $ Fst $ VarN Here) (CoVarN Here)

-- Intro for positive product
posPair : {a, b : Ty Set} -> Cmd [a, b] Set [Ten a b]
posPair = CPos (Val $ Pair (VarP Here) (VarP $ There Here)) (CoVarP Here)

-- Elimination for a negative sum
usePar : {a, b : Ty Op} -> Cmd [Par a b] Op [a, b]
usePar = CNeg (CoVal $ Para (VarN Here) (VarN $ There Here)) (CoVarN Here)