--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--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.h.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