Changes between Version 12 and Version 13 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 6:00:18 PM (5 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