{-# Language TypeFamilies, RankNTypes, UndecidableInstances, TypeOperators, ImportQualifiedPost, DataKinds #-}
{-|
Module      : Advent.Nat
Description : Type level nats as successor and zero
Copyright   : (c) Eric Mertens, 2021
License     : ISC
Maintainer  : emertens@gmail.com

-}
module Advent.Nat where

import GHC.TypeNats qualified as T

-- | Natural numbers (used for type index)
data Nat
  = Z     -- ^ zero
  | S Nat -- ^ successor

-- | Covert from GHC type literal syntax to an inductively defined natural
type family FromNatural (n :: T.Natural) :: Nat where
  FromNatural 0 = 'Z
  FromNatural n = 'S (FromNatural (n T.- 1))

class UnfoldNat n where
  unfoldNat :: f 'Z -> (forall m. f m -> f ('S m)) -> f n

instance UnfoldNat 'Z where
  unfoldNat :: forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f 'Z
unfoldNat f 'Z
z forall (m :: Nat). f m -> f ('S m)
_ = f 'Z
z

instance UnfoldNat n => UnfoldNat ('S n) where
  unfoldNat :: forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f ('S n)
unfoldNat f 'Z
z forall (m :: Nat). f m -> f ('S m)
s = f n -> f ('S n)
forall (m :: Nat). f m -> f ('S m)
s (f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f n
forall (n :: Nat) (f :: Nat -> *).
UnfoldNat n =>
f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f n
unfoldNat f 'Z
z f m -> f ('S m)
forall (m :: Nat). f m -> f ('S m)
s)