Changes between Version 18 and Version 19 of TypeNats/Basics


Ignore:
Timestamp:
Jan 31, 2011 9:37:35 AM (3 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v18 v19  
    5959  where check y = if x == natToInteger y then Just y else Nothing 
    6060}}} 
     61It checks that the value argument `x`, passed at runtime, matches the statically-expected value, returning `Nothing` if not, and a typed singleton if so. 
    6162 
    6263The implementation of `integerToMaybeNat` is a little subtle: by using 
     
    6465`nat` (aka `y`) both have the same type, namely `Nat n`.  There are other 
    6566ways to achieve the same, for example, by using scoped type variables, 
    66 and providing explicit type signatures. 
     67thus: 
     68{{{ 
     69integerToMaybeNat :: forall n. NatI n => Integer -> Maybe (Nat n) 
     70integerToMaybeNat x  
     71  | x == natToInteger (nat :: Nat n) = Just nat  
     72  | otherwise                        = Nothing 
     73}}} 
    6774 
    6875Now, we can use `integerToNat` to provide a `Read` instance for singleton types: