{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
-----------------------------------------------------------------------------
-- |
-- Module : Type.Family.Nat
-- Copyright : Copyright (C) 2015 Kyle Carter
-- License : BSD3
--
-- Maintainer : Kyle Carter <kylcarte@indiana.edu>
-- Stability : experimental
-- Portability : RankNTypes
--
-- Type-level natural numbers, along with frequently used
-- type families over them.
--
-----------------------------------------------------------------------------
module Type.Family.Nat
( module Type.Family.Nat
, type (==)
) where
import Data.Type.Equality
import Type.Family.List
data N
= Z
| S N
deriving (Eq,Ord,Show)
type family NatEq (x :: N) (y :: N) :: Bool where
NatEq Z Z = True
NatEq Z (S y) = False
NatEq (S x) Z = False
NatEq (S x) (S y) = NatEq x y
type instance x == y = NatEq x y
type family Iota (x :: N) :: [N] where
Iota Z = Ø
Iota (S x) = x :< Iota x
type family Pred (x :: N) :: N where
Pred (S n) = n
type family (x :: N) + (y :: N) :: N where
Z + y = y
S x + y = S (x + y)
infixr 6 +
type family (x :: N) * (y :: N) :: N where
Z * y = Z
S x * y = (x * y) + y
infixr 7 *
type family (x :: N) ^ (y :: N) :: N where
x ^ Z = S Z
x ^ S y = (x ^ y) * x
infixl 8 ^
-- | Convenient aliases for low-value Peano numbers.
type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7
type N9 = S N8
type N10 = S N9