Changes between Version 27 and Version 28 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 1:18:01 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v27 v28  
    1 == Type-Level Naturals ==
     1== Type-Level Literals ==
    22
    3 There is a new kind, `Nat`.  It is completely separate from GHC's hierarchy of sub-kinds, so `Nat` is only a sub-kind of itself.
     3Currently, we support two forms of type-level literals: natural numbers, and symbol constants.
     4Natural number literals are a family of types, all of which belong to the kind `Nat`.  Similarly,
     5symbol literals are types that belong to the kind `Symbol`:
    46
    5 The inhabitants of `Nat` are an infinite family of (empty) types, corresponding to the natural numbers:
    67{{{
    780, 1, 2, ... :: Nat
     9"hello", "world", "some string literal" :: Symbol
    810}}}
    911
    10 These types are linked to the value world by a small library with the following API:
     12Both of numeric and symbol literal types are empty---they have no inhabitants.  However, they may be
     13used as parameters to other type constructors, which makes them useful.
     14
     15
     16== Singleton Types ==
     17
     18We use this idea to link the type-level literals to specific run-time values via //singleton types//.
     19The singleton types and some useful functions for working with them are defined in module {{{GHC.TypeLits}}}:
     20
    1121{{{
    1222module GHC.TypeLits where
    1323}}}
    1424
    15 == Singleton Types ==
     25A //singleton type// is simply a type that has only one interesting inhabitant.  We define a whole family
     26of singleton types, parameterized by type-level literals:
     27{{{
     28newtype Sing :: a -> *
     29}}}
     30So, for example, {{{Sing 0}}}, {{{Sing 127}}}, {{{Sing "hello"}}}, {{{Sing "this also}}}}, are all
     31singleton types.  The idea is that the only inhabitant of {{{Sing n}}} is the value {{{n}}}.  Notice
     32that {{{Sing}}} has a //polymorphic kind// because sometimes we apply it to numbers (which are of
     33kind {{{Nat}}}) and sometimes we apply it to symbols (which are of kind {{{Symbol}}}).
     34
     35But, if we have a value of type {{{Sing a}}}, how do we get the actual integer or string?
     36We can do this with the function {{{fromSing}}}:
     37{{{
     38fromSing :: Sing a -> SingRep a
     39
     40type family SingRep a
     41type instance SingRep (n :: Nat)    = Integer
     42type instance SingRep (n :: Symbol) = String
     43}}}
     44
     45While the type of {{{fromSing}}} looks a bit complex at first it is actually quite simple:
     46given a singleton type, it will return either an integer or a string, depending on the //kind// of
     47its index.  So, if we apply it to a value of type {{{Sing 3}}} we would get the number {{{3}}}, but,
     48if we apply to a value of type {{{Sing "hello"}}} we would get the string "hello".
     49
    1650
    1751We relate type-level natural numbers to run-time values via a family of singleton types: