--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--Module       : Type.Nat
--Author       : Daniel Schüssler
--License      : BSD3
--Copyright    : Daniel Schüssler
--
--Maintainer   : Daniel Schüssler
--Stability    : Experimental
--Portability  : Uses various GHC extensions
--
--------------------------------------------------------------------------------
--Description  : 
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------



{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS -Wall #-}

-- | TODO
--
-- * Prove that 'Initor' is an 'NMorphism'
--
-- * Prove that it is uniquely so
--
module Type.Nat where

import Type.Set
import Type.Dummies()
import Type.Function
import Type.Logic()
import Data.Type.Equality
import Control.Monad()
import Control.Exception

#include "../Defs.hs"
         
-- | Sets equipped with a constant and a function to itself
data NStructure set z succ where
                  NStructure :: z :∈: set -> (set :~>: set) succ ->
                               NStructure set z succ

-- | Structure-preserving maps of 'NStructure's
data NMorphism set1 z1 succ1 set2 z2 succ2 (f :: SET) where
    NMorphism :: NStructure set1 z1 succ1 ->
                NStructure set2 z2 succ2 ->
                (set1 :~>: set2) f ->
                (f z1 :=: z2) ->
                (f :○: succ1 
                 :==:
                 succ2 :○: f) ->

                NMorphism set1 z1 succ1 z2 set2 succ2 f
                          
-- | Expresses that @(set1,z1,succ1)@ is initial in the cat of 'NStructure's, in other words, that it is isomorphic to the natural numbers
data NInitial set1 z1 succ1 where
    NInitial :: (forall z2 set2 succ2. ExUniq1 (NMorphism set1 z1 succ1 z2 set2 succ2))
               -> NInitial set1 z1 succ1
                 

-- data IsPeano nat z succ = 
--     IsPeano {
--       succ_fun :: (nat :~>: nat) succ
--     , succ_inj :: Injective succ
--     , not_succ_zero :: forall n. n :∈: nat -> Not ((n,z) :∈: succ)
--     , induction :: forall set. z :∈: set -> 
--                   (forall n n1. n :∈: set ->   
--                            (n,n1) :∈: succ ->
--                            n1 :∈: set) ->

--                   set :==: nat
--     }

-- | Actually any pair of (nullary type, unary type constructor) gives us a copy of the naturals; let's call these /TNats/
data TNat z s :: SET where
    IsZ :: TNat z s z
    IsS :: TNat z s n -> TNat z s (s n)
-- | Successor function made from a unary type constructor
data Succ z s :: SET where 
    Succ :: n :∈: TNat z s -> Succ z s (n,s n)
           
succFun :: (TNat z s :~>: TNat z s) (Succ z s)
succFun = IsFun (Subset (\(Succ n) -> n :×: IsS n))
          (ExSnd . Succ)
          (\(Succ _) (Succ _) k -> k)
          
tyconNStruct :: NStructure (TNat z s) z (Succ z s)
tyconNStruct = NStructure IsZ succFun
               
-- | The unique morphism from an 'TNat' to any 'NStructure' 
--
-- NB: @s@ is a type constructor, but @succ2@ is a Function ('IsFun')
data Initor z s z2 succ2 :: SET where
      InitorZ :: Initor z s z2 succ2 (z,z2)
      InitorS :: Initor z s z2 succ2 (n1, n2) -> 
                (n2,sn2) :∈: succ2 ->
                Initor z s z2 succ2 (s n1, sn2)
                       

initorFun :: forall z s set2 z2 succ2. NStructure set2 z2 succ2 -> 
            (TNat z s :~>: set2) (Initor z s z2 succ2)
                                
initorFun (NStructure z2 succ2) =

    let 
        prelation :: pair :∈: Initor z s z2 succ2 -> 
                         pair :∈: TNat z s :×: set2
                              
        prelation InitorZ = IsZ :×: z2
        prelation (InitorS i0 p) = case prelation i0 of
                                          q1 :×: _ -> 
                                                 IsS q1 
                                                    :×: 
                                                 inCod succ2 p
                                                       
        ptotal :: n :∈: TNat z s -> ExSnd (Initor z s z2 succ2) n
        ptotal IsZ = ExSnd InitorZ
        ptotal (IsS n) = 
            case ptotal n of
              ExSnd (inn2 :: Initor z s z2 succ2 (n,n2)) -> 
                  
                         (let
                             succ2ofn2 :: ExSnd succ2 n2
                             succ2ofn2 =
                                 case prelation inn2 of
                                   _ :×: n2 ->
                                       total succ2 n2
                          in
                           case succ2ofn2 of 
                             ExSnd e -> ExSnd (InitorS inn2 e))
                         
        psval :: Initor z s z2 succ2 (n,n2) ->
                Initor z s z2 succ2 (m,m2) ->
                    n2 :=: m2
                       
        psval InitorZ InitorZ = Refl
        psval (InitorS inn2 succ2n2) (InitorS inn2' succ2'n2') = 
            case psval inn2 inn2' of
              Refl ->
                  case sval succ2 succ2n2 succ2'n2' of
                    Refl -> Refl
                           
        -- Currently impossible without 'undefined' :-(

        -- http://www.nabble.com/Is-it-possible-to-prove-type-*non*-equality-in-Haskell--to25142999.html 
        psval (InitorS _ _) InitorZ = assert False undefined
        psval InitorZ (InitorS _ _) = assert False undefined
     in
       IsFun (Subset prelation) ptotal (\p1 p2 k -> case psval p1 p2 of 
                                                     Refl -> k)


-- tyconPeano :: IsPeano (TNat z s) z (Succ z s)
-- tyconPeano = IsPeano succFun
--              (Injective (\(Succ _) (Succ _) k -> k))
             
--              undefined undefined