Agda model of Serrano, Miraldo, "Generic Programming of All Kinds: Type Constructors and GADTs in Sum-of-Products Style"

GenericNSOP.idr

module GenericNSOP

import Data.List.Quantifiers

%default total
%access public export

data K = Star | Arr K K

interpK : K -> Type
interpK Star = Type
interpK (Arr k1 k2) = interpK k1 -> interpK k2

data TyVar : K -> K -> Type where
  VZ : TyVar (Arr k ks) k
  VS : TyVar ks k -> TyVar (Arr k' ks) k

data Atom : K -> K -> Type where
  Var : TyVar z k1 -> Atom z k1
  Kon : interpK k1 -> Atom z k1
  App : Atom z (Arr k1 k2) -> Atom z k1 -> Atom z k2
  --Rec : Atom k k

data G : K -> Type where
  GZ : G Star
  GS : interpK k1 -> G k2 -> G (Arr k1 k2)

Ty : G k -> Atom k res -> interpK res
Ty  GZ       (Var  VZ)    impossible
Ty  GZ       (Var (VS _)) impossible
Ty (GS g1 g) (Var  VZ)    = g1
Ty (GS g1 g) (Var (VS v)) = Ty g (Var v)
Ty  g        (Kon x)      = x
Ty  g        (App f x)    = Ty g f (Ty g x)

data Field : K -> Type where
  Explicit : Atom k Star -> Field k
  Implicit : (G k -> Type) -> Field k

interpF : Field k -> G k -> Type
interpF (Explicit t) g = Ty g t
interpF (Implicit ctr) g = ctr g

Prod : K -> Type
Prod = List . Field

interpP : Prod k -> G k -> Type
interpP as g = All (\a => interpF a g) as

SoP : K -> Type
SoP = List . Prod

interpS : SoP k -> G k -> Type
interpS ps g = Any (\p => interpP p g) ps

data IsNat : Type -> Type where
  Prf : Nat -> IsNat Nat

isnatSOP : SoP (Arr Star Star)
isnatSOP = [[Implicit ctr, Explicit (Var VZ)]]
  where
  ctr : G (Arr Star Star) -> Type
  ctr (GS x GZ) = x=Nat