Changes between Version 7 and Version 8 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Mar 21, 2012 1:37:19 AM (2 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}}}