Changes between Version 18 and Version 19 of TypeNats/Basics


Ignore:
Timestamp:
Jan 31, 2011 9:37:35 AM (5 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: