Commit 02998bd6 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

Add unary natural numbers to experiment on matching with literals.

The idea is that when we want to match on type level nats, we should
use `Nat1`, and use the `FromNat1` function to switch between the
structured and unstructured representation of numbers.

A bit of custom machinery is needed for this to work properly,
because to go back (i.e., to solve FromNat1 x ~ 3) GHC needs to know
that FromNat1 is an injective function.
parent 4f03d110
......@@ -31,9 +31,12 @@ module GHC.TypeLits
-- * Functions on type nats
, type (<=), type (<=?), type (+), type (*), type (^)
-- * Destructing type-nats.
-- * Destructing type-nat singletons.
, isZero, IsZero(..)
, isEven, IsEven(..)
-- * Matching on type-nats
, Nat1(..), FromNat1
) where
import GHC.Base(Eq((==)), Bool(..), ($), otherwise, (.))
......@@ -186,3 +189,14 @@ instance Show (IsEven n) where
show (IsOdd x) = "(2 * " ++ show x ++ " + 1)"
--------------------------------------------------------------------------------
-- | Unary implemenation of natural numbers.
-- Used both at the type and at the value level.
data Nat1 = Zero | Succ Nat1
type family FromNat1 (n :: Nat1) :: Nat
type instance FromNat1 Zero = 0
type instance FromNat1 (Succ n) = 1 + FromNat1 n
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment