Changes between Version 32 and Version 33 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 2:08:12 AM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v32 v33  
    4949 
    5050So, how do we make values of type `Sing n` in the first place?  This is done with 
    51 a the special overloaded constant `sing`: 
     51the special overloaded constant `sing`: 
    5252{{{ 
    5353class SingI a where 
    5454  sing :: Sing a 
    5555 
    56 -- Built-in instances for all type0literals. 
    57 instance SingI 0        where sing = // ... the singleton value representing 0 ... 
    58 instance SingI 1        where sing = // ... the singleton value representing 1 ... 
    59 instance SingI "hello"  where sing = // ... the singleton value representing "hello" ... 
     56-- Built-in instances for all type-literals. 
     57instance SingI 0        where sing = ... the singleton value representing 0 ... 
     58instance SingI 1        where sing = ... the singleton value representing 1 ... 
     59instance SingI "hello"  where sing = ... the singleton value representing "hello" ... 
    6060// ... etc. 
    6161}}} 
     62 
     63Here are some examples on the GHCi prompt to get a feel of how `sing` works: 
     64{{{ 
     65> :set -XDataKinds 
     66> sing :: Sing 1 
     67> 1 
     68> sing :: Sing "hello" 
     69> "hello" 
     70}}} 
     71 
     72The name ''SingI'' is a mnemonic for the different uses of the class: 
     73  * It is the ''introduction'' construct for 'Sing' values, 
     74  * It is an ''implicit'' singleton parameter (this is discussed in more detail bellow) 
     75 
     76Notice that GHCi could display values of type `Sing`, so they have a `Show` instance.  As another example, here 
     77is the definition of the `Show` instance: 
     78{{{ 
     79instance Show (SingRep a) => Show (Sing a) where 
     80  showsPrec p = showsPrec p . fromSing 
     81}}} 
     82Easy! We just convert the singleton into an ordinary value (integer or string), and use ''its'' `Show` instance to display it. 
     83 
     84Next, we show two functions which make it easier to work with singleton types: 
     85 
     86{{{ 
     87withSing :: SingI a => (Sing a -> b) -> b 
     88withSing f = f sing 
     89 
     90singThat :: SingI a => (SingRep a -> Bool) -> Maybe (Sing a) 
     91singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing 
     92}}} 
     93 
     94The first function, `withSing`, is useful when we want to work with the same singleton value multiple times. 
     95The constant `sing` is polymorphic, so every time we use it in a program, it may refer to a potentially 
     96different singleton, so to ensure that two singleton values are the same we have to resort to 
     97explicit type signatures, which just adds noise to a definition.  By using, `withSing` we avoid this problem 
     98because we get an explicit (monomorphic) name for a given singleton, and so we can use the name many times 
     99without any type signatures.  This technique is shown in the definition of the second function, `singThat`. 
     100 
     101The function `singThat` is similar to the constant `sing` in that it defines new singleton values. However, 
     102it allows us to specify a predicate on (the representation of) the value and it only succeeds if this predicate 
     103holds.  Here are some examples of how that works: 
     104 
     105{{{ 
     106> singThat (== 1) :: Maybe (Sing 1) 
     107> Just 1 
     108> singThat (== 1) :: Maybe (Sing 2) 
     109> Nothing 
     110> singThat ("he" `isPrefixOf`) :: Maybe (Sing "hello") 
     111> Just "hello" 
     112}}} 
     113 
     114Now, using `singThat` we can show the definition of the `Read` instance for singletons: 
     115 
     116{{{ 
     117instance (SingI a, Read (SingRep a), Eq (SingRep a)) => Read (Sing a) where 
     118  readsPrec p cs = do (x,ys) <- readsPrec p cs 
     119                      case singThat (== x) of 
     120                        Just y  -> [(y,ys)] 
     121                        Nothing -> [] 
     122}}} 
     123 
     124We use the `Read` instance of the representation for the singletons to parse a value, 
     125and then, we use `singThat` to make sure that this was the value corresponding to 
     126the singleton. 
    62127 
    63128 
    64129 
    65130 
    66 We relate type-level natural numbers to run-time values via a family of singleton types: 
    67 {{{ 
    68 data TNat :: Nat -> * 
    69131 
    70 tNat         :: NatI n => TNat n 
    71 tNatInteger  :: TNat n -> Integer 
    72132 
    73 -- Convenient derived functions 
    74 tNatThat     :: NatI n => (Integer -> Bool) -> Maybe (TNat n) 
    75 withTNat     :: NatI n => (TNat n -> a) -> a 
    76 }}} 
    77 The only "interesting" value of type {{{TNat n}}} is the number {{{n}}}.  Technically, there is also an undefined element. 
    78 The value of a singleton type may be named using {{{tNat}}}, which is a bit like a "smart" constructor for {{{TNat n}}}. 
    79 Note that because {{{tNat}}} is polymorphic, we may have to use a type signature to specify which singleton we mean.  For example: 
    80  
    81 One may think of the smart constructor {{{tNat}}} as being a method of a special built-in class, {{{NatI}}}: 
    82 {{{ 
    83 class NatI n where 
    84   tNat :: TNat n 
    85  
    86 instance NatI 0 where tNat = ...singleton 0 value... 
    87 instance NatI 1 where tNat = ...singleton 1 value... 
    88 instance NatI 2 where tNat = ...singleton 2 value... 
    89 etc. 
    90 }}} 
    91  
    92 The name ''NatI'' is a mnemonic for the different uses of the class: 
    93   * It is the ''introduction'' construct for 'TNat' values, 
    94   * It is an ''implicit'' parameter of kind 'TNat' (this is discussed in more detail bellow) 
    95133 
    96134== Examples ==