-------------------------------------------------------------
-- |
-- Module : Data.Nat
-- Copyright : (C) 2015, Yu Fukuzawa
-- License : BSD3
-- Maintainer : minpou.primer@email.com
-- Stability : experimental
-- Portability : portable
--
-----------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Nat where
data Nat = Z | S Nat
data SNat (n :: Nat) where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
class SingNat (n :: Nat) where
singNat :: SNat n
instance SingNat Z where
singNat = SZ
{-# INLINE singNat #-}
instance SingNat n => SingNat (S n) where
singNat = SS singNat
{-# INLINE singNat #-}
type family (:+:) (n :: Nat) (m :: Nat) where
Z :+: n = n
S n :+: m = S (n :+: m)
type family (:-:) (n :: Nat) (m :: Nat) where
n :-: Z = n
S n :-: S m = n :-: m
class (:<=) (n :: Nat) (m :: Nat) where
instance (:<=) Z n
instance (n :<= m) => (:<=) (S n) (S m)