Changes between Version 27 and Version 28 of TypeNats/Basics


Ignore:
Timestamp:
Apr 9, 2012 1:18:01 AM (2 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: