Changes between Version 27 and Version 28 of TypeNats/Basics
 Timestamp:
 Apr 9, 2012 1:18:01 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

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