Changes between Version 32 and Version 33 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 2:08:12 AM (3 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 ==