My.idr

module Exercises.My

import Data.Vect

%default total

public export
data CFT : Nat -> Type where
  Var   : Fin n -> CFT n
  Zero  : CFT n
  One   : CFT n
  Plus  : CFT n -> CFT n -> CFT n
  Times : CFT n -> CFT n -> CFT n
  Mu    : CFT (S n) -> CFT n

record Fix (f : Type -> Type) where
  constructor In
  unFix : Inf (f (Fix f))

ToType : CFT n -> Vect n Type  -> Type
ToType (Var x) xs = index x xs
ToType Zero xs = Void
ToType One xs = Unit
ToType (Plus x y) xs = Either (ToType x xs) (ToType y xs)
ToType (Times x y) xs = Pair (ToType x xs) (ToType y xs)
ToType (Mu x) xs = Fix (\self => ToType x (self :: xs))

NatDesc : CFT Z
NatDesc = Mu(One `Plus` Var 0)

NatTy : Type
NatTy = ToType NatDesc []

ListDesc : CFT (S n)
ListDesc = Mu(One `Plus` (Var 1 `Times` Var 0))

ListTy : Type -> Type
ListTy ty = ToType ListDesc [ty]

TreeDesc : CFT (S n)
TreeDesc = Mu(One `Plus` (Var 1 `Times` (Var 0 `Times` Var 0)))

TreeTy : Type -> Type
TreeTy ty = ToType TreeDesc [ty]