blob: cb3c8e8e5655b51253f49574e81ea2fd60f189ad (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Numerals where
import Data.Kind
data Z -- empty data type
data S a -- empty data type
data SNat n where -- natural numbers as singleton type
Zero :: SNat Z
Succ :: SNat n -> SNat (S n)
zero = Zero
one = Succ zero
two = Succ one
three = Succ two
-- etc...we really would like some nicer syntax here
type family (:+:) n m :: Type
type instance Z :+: m = m
type instance (S n) :+: m = S (n :+: m)
add :: SNat n -> SNat m -> SNat (n :+: m)
add Zero m = m
add (Succ n) m = Succ (add n m)
|
