blob: 17fb30c3cae0c40ce0af4ac4d6d6fa8f1a4b70e8 (
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
|
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Numerals
where
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 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)
|
