Changes between Version 12 and Version 13 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 6:00:18 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v12 v13  
    4545  * It is an ''implicit'' parameter of kind 'Nat' (this is discussed in more detail in [wiki:TypeNats/ImplicitExplicit a separate section]) 
    4646 
     47== Examples == 
     48 
     49Here is how we can use this API to define a `Show` instance for singleton types: 
     50{{{ 
     51instance Show (Nat n) where 
     52  showsPrec p n = showsPrec p (natToInteger n) 
     53}}} 
     54 
     55A more interesting example is to define a function which maps integers into singleton types: 
     56{{{ 
     57integerToMaybeNat :: TypeNat n => Integer -> Maybe (Nat n) 
     58integerToMaybeNat x = check nat 
     59  where check y = if x == natToInteger y then Just y else Nothing 
     60}}} 
     61 
     62The implementation of `integerToMaybeNat` is a little subtle: by using 
     63the helper function `check`, we ensure that the two occurrences of 
     64`nat` (aka `y`) both have the same type, namely `Nat n`.  There are other 
     65ways to achieve the same, for example, by using scoped type variables, 
     66and providing explicit type signatures. 
     67 
     68Now, we can use `integerToNat` to provide a `Read` instance for singleton types: 
     69{{{ 
     70instance TypeNat n => Read (Nat n) where 
     71  readsPrec p x       = do (x,xs) <- readsPrec p x 
     72                           case integerToMaybeNat x of 
     73                             Just n  -> [(n,xs)] 
     74                             Nothing -> [] 
     75}}} 
     76 
    4777 
    4878