{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Peano
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.NNO where

import Data.Kind (Type)

import Data.Category.Functor
import Data.Category.Limit
import Data.Category.Unit
import Data.Category.Coproduct
import Data.Category.Fix (Fix(..))


class HasTerminalObject k => HasNaturalNumberObject k where

  type NaturalNumberObject k :: Type

  zero :: k (TerminalObject k) (NaturalNumberObject k)
  succ :: k (NaturalNumberObject k) (NaturalNumberObject k)

  primRec :: k (TerminalObject k) a -> k a a -> k (NaturalNumberObject k) a


data NatNum = Z | S NatNum

instance HasNaturalNumberObject (->) where

  type NaturalNumberObject (->) = NatNum

  zero :: TerminalObject (->) -> NaturalNumberObject (->)
zero = \() -> NatNum
Z
  succ :: NaturalNumberObject (->) -> NaturalNumberObject (->)
succ = NatNum -> NatNum
S

  primRec :: forall a.
(TerminalObject (->) -> a)
-> (a -> a) -> NaturalNumberObject (->) -> a
primRec TerminalObject (->) -> a
z a -> a
_  NatNum
NaturalNumberObject (->)
Z    = TerminalObject (->) -> a
z ()
  primRec TerminalObject (->) -> a
z a -> a
s (S NatNum
n) = a -> a
s (forall (k :: * -> * -> *) a.
HasNaturalNumberObject k =>
k (TerminalObject k) a -> k a a -> k (NaturalNumberObject k) a
primRec TerminalObject (->) -> a
z a -> a
s NatNum
n)


-- type Nat = Fix ((:++:) Unit)

-- instance HasNaturalNumberObject Cat where

--   type NaturalNumberObject Cat = CatW Nat

--   zero = CatA (Const (Fix (I1 Unit)))
--   succ = CatA (Wrap :.: Inj2)

--   primRec (CatA z) (CatA s) = CatA (PrimRec z s)

-- data PrimRec z s = PrimRec z s
-- instance (Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s) where
--   type Dom (PrimRec z s) = Nat
--   type Cod (PrimRec z s) = Cod z
--   type PrimRec z s :% I1 () = z :% ()
--   type PrimRec z s :% I2 n  = s :% PrimRec z s :% n
--   PrimRec z _ % Fix (I1 Unit) = z % Unit
--   PrimRec z s % Fix (I2 n) = s % PrimRec z s % n