data-category-0.11: Data/Category/NNO.hs

{-# 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 = \() -> Z
  succ = S

  primRec z _  Z    = z ()
  primRec z s (S n) = s (primRec z s 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