{-# OPTIONS --disable-positivity-check #-}
module Homogenous.Base where
-- module Homogenous.Base(Arity, Sig, T, Intro) where

import TYPE
import Prelude

open Prelude using
  (Absurd
   Unit unit
   Nat  zero suc
   List nil _::_
   Either  left right
   Pair pair)

-- A homogenous algebra can be represented by a list of arities
--   (natural numbers)

Arity : Set
Arity = Nat

Sig   : Set
Sig   = List Arity

-- Many definitions below come in pairs - one for Arity and one for
-- Sig - where name of the first one ends in a (as in Arity):
--   funa : Arity -> ...
--   fun  : Sig -> ...

-- (Fa n,Fa1 n) is the functor "n-tuple of same type" or
--                 "vector of length n" or "(^n)"

Fa : (n:Arity) -> Set -> Set
Fa (zero)  X = Unit
Fa (suc m) X = Pair X (Fa m X)

 ----------------------------------------------------------------
Fa1 : (n:Arity) -> {a b:Set} -> (a -> b) -> Fa n a -> Fa n b
Fa1 (zero)  f (unit)         = unit
Fa1 (suc m) f (pair fst snd) = pair (f fst) (Fa1 m f snd)

-- (F fi, F1 fi) is the pattern functor for a homogenous algebra

F : (fi:Sig)(X:Set) -> Set
F (nil)      X = Absurd
F (n :: fi') X = Either (Fa n X) (F fi' X)

F1 : (fi:Sig){a b:Set}(f:a -> b)(x:F fi a) -> F fi b
F1 (nil)      f ()        -- empty
F1 (n :: ns)  f (left  t) = left  (Fa1 n f t)
F1 (n :: ns)  f (right y) = right (F1 ns f y)

-- For the definition of the recursor R we need family-level
-- variants of F and F1: FIH and Fmap. As usual we define these first
-- for arities (with a postfix 'a' in the name) and then for signatures.

FIHa : (n:Arity){X:Set}(C:X -> Set)(x:Fa n X) -> Set
FIHa (zero)  C unit           = Unit
FIHa (suc m) C (pair fst snd) = Pair (C fst) (FIHa m C snd)

FIH : (fi:Sig){X:Set}(C:X -> Set)(x:F fi X) -> Set
FIH (nil)      C ()      -- empty
FIH (n :: ns)  C (left  t) = FIHa n C t
FIH (n :: ns)  C (right y) = FIH ns C y

Fmapa : (n:Arity){X:Set}{C:X -> Set}(h:(x:X) -> C x)(u:Fa n X)
      -> FIHa n C u
Fmapa (zero)  h (unit)         = unit
Fmapa (suc m) h (pair fst snd) = pair (h fst) (Fmapa m h snd)

Fmap : (fi:Sig){X:Set}{C:X -> Set}(h:(x:X) -> C x)(u:F fi X)
     -> FIH fi C u
Fmap (nil)      h () -- empty
Fmap (n :: ns)  h (left  x) = Fmapa n h x
Fmap (n :: ns)  h (right y) = Fmap ns h y

-- Finally the homogenous algebra construction itself - for each code
-- fi there is a datatype T fi and an iterator It fi

data T (fi:Sig) : Set where
  Intro : F fi (T fi) -> T fi

It : (fi:Sig){C:Set}(d:F fi C -> C) -> T fi -> C
It fi d (Intro i) = d (F1 fi (It fi d) i)

-- Mendler style iterator is also straight forward

MIt : (fi:Sig){C:Set}(s:{X:Set} -> (X -> C) -> F fi X -> C)
    -> T fi -> C
MIt fi s (Intro i) = s (MIt fi s) i

R : (fi:Sig)
    {C:T fi -> Set}
    (d:(y:F fi (T fi)) -> FIH fi C y -> C (Intro y))
    (x:T fi) -> C x
R fi d (Intro i) = d i (Fmap fi (R fi d) i)

-- Special case of FIH

FIHs : (fi:Sig) -> (T fi -> Set) -> F fi (T fi) -> Set
FIHs fi = FIH fi

-- A simple example: the inverse of Intro

out : (fi:Sig) -> T fi -> F fi (T fi)
out fi = R fi (\y p -> y)

----------------------------------------------------------------
-- Now for the Type level: define FIHa, FIH, Fmapa, Fmap again
--   (universe polymorphism, please!)

FIHaT : (n:Arity)(X:Set)(C:X -> Set1)(x:Fa n X) -> Set1
FIHaT (zero)  X C (unit)         = TYPE.Unit
FIHaT (suc m) X C (pair fst snd) = TYPE.Pair (C fst) (FIHaT m X C snd)


FIHT : (fi:Sig)(X:Set)(C:X -> Set1)(x:F fi X) -> Set1
FIHT (nil)      X C () -- empty
FIHT (n :: ns)  X C (left  t) = FIHaT n X C t
FIHT (n :: ns)  X C (right y) = FIHT ns X C y

FIHsT : (fi:Sig)(C:T fi -> Set1)(x:F fi (T fi)) -> Set1
FIHsT fi C x = FIHT fi (T fi) C x

FmapaT : (n:Arity){X:Set}{C:X -> Set1}(h:(x:X) -> C x)(u:Fa n X)
  -> FIHaT n X C u
FmapaT (zero)  h (unit)         = TYPE.unit
FmapaT (suc m) h (pair fst snd) = TYPE.pair (h fst) (FmapaT m h snd)

FmapT : (fi:Sig){X:Set}{C:X -> Set1}(h:(x:X) -> C x)(u:F fi X)
      -> FIHT fi X C u
FmapT (nil)      h () -- empty
FmapT (n :: ns)  h (left  x') = FmapaT n h x'
FmapT (n :: ns)  h (right y)  = FmapT ns h y

RT : (fi:Sig)
     {C:T fi -> Set1}
     (d:(y:F fi (T fi)) -> FIHT fi (T fi) C y -> C (Intro y))
     (x:T fi) -> C x
RT fi d (Intro i) = d i (FmapT fi (RT fi d) i)