Changes between Version 7 and Version 8 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Mar 21, 2012 1:37:19 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/InductiveDefinitions

    v7 v8  
     1The module {{{GHC.TypeLits}}} provides two views on values of type {{{TNat}}},
     2which make it possible to define inductive functions using {{{TNat}}} values.
     3
     4== Checking for Zero (Unary Strucutre of Nat) ==
     5
     6The first view provides the same functionality as usual
     7Peano arithmetic definition of the natural numbers.  It
     8is useful when using {{{TNat}}} to count something.
    19{{{
    2 {-# LANGUAGE TypeNaturals, GADTs #-}
     10isZero :: TNat n -> IsZero n
    311
    4 import GHC.TypeNats
    5 import Unsafe.Coerce
     12data IsZero :: Nat -> * where
     13  IsZero ::              IsZero 0
     14  IsSucc :: !(TNat n) -> IsZero (n + 1)
     15}}}
    616
    7 --------------------------------------------------------------------------------
    8 -- Extending GHC.TypeNats with these two declarations allows us to
    9 -- write inductive definitions.
    10 
    11 data UNat :: Nat -> * where
    12   Zero :: UNat 0
    13   Succ :: UNat n -> UNat (n + 1)
    14 
    15 toUNat :: Nat n -> UNat n
    16 toUNat n = unsafe (natToInteger n)
    17   where unsafe :: Integer -> UNat n
    18         unsafe 0 = unsafeCoerce Zero
    19         unsafe n = unsafeCoerce (Succ (unsafe $! (n-1)))
    20 
    21 --------------------------------------------------------------------------------
    22 
    23 data Vec :: Nat -> * -> * where
    24   Nil  :: Vec 0 a
    25   Cons :: a -> Vec n a -> Vec (n + 1) a
    26 
    27 instance Show a => Show (Vec n a) where
    28   show Nil = "[]"
    29   show (Cons x xs) = show x ++ " : " ++ show xs
    30 
    31 instance Functor (Vec n) where
    32   fmap f Nil          = Nil
    33   fmap f (Cons x xs)  = Cons (f x) (fmap f xs)
    34 
    35 cat :: Vec m a -> Vec n a -> Vec (m + n) a
    36 cat Nil ys          = ys
    37 cat (Cons x xs) ys  = Cons x (cat xs ys)
    38 
    39 vecLen :: NatI n => Vec n a -> Nat n
    40 vecLen _ = nat
     17By using {{{isZero}}} we can check if a number is 0 or the successor
     18of another number.  The interesting aspect of {{{isZero}}} is that
     19the result is typed:  if {{{isZero x}}} returns {{{IsSucc y}}},
     20then the type checker knows that the type of {{{y}}} is one smaller
     21then {{{x}}}.
    4122
    4223
    43 splitU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    44 splitU Zero xs               = (Nil, xs)
    45 splitU (Succ n) (Cons x xs)  = let (as,bs) = splitU n xs
    46                                in (Cons x as, bs)
     24== Checking for Evenness (Binary Structure of Nat) ==
    4725
    48 vecSplitAt :: Nat m -> Vec (m + n) a -> (Vec m a, Vec n a)
    49 vecSplitAt n = splitU (toUNat n)
     26The other view provides a more "bit-oriented" view of
     27the natural numbers, by allowing is to check if the least
     28significant bit of a number is 0 or 1.  It is useful
     29when we use {{{TNat}}} values for splitting things
     30in half:
     31{{{
     32isEven :: TNat n -> IsEven n
    5033
    51 vecSplit :: NatI m => Vec (m + n) a -> (Vec m a, Vec n a)
    52 vecSplit = vecSplitAt nat
     34data IsEven $a where
     35  IsEvenZero ::                    IsEven 0
     36  IsEven     :: !(TNat (n + 1)) -> IsEven (2 * (n + 1))
     37  IsOdd      :: !(TNat n)       -> IsEven ((2 * n) + 1)
    5338}}}