Changes between Version 31 and Version 32 of TypeNats/Basics
 Timestamp:
 Apr 9, 2012 1:39:19 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Basics
v31 v32 28 28 newtype Sing :: a > * 29 29 }}} 30 So, for example, {{{Sing 0}}}, {{{Sing 127}}}, {{{Sing "hello"}}}, {{{Sing "this also}}}}, are all30 For example, {{{Sing 0}}}, {{{Sing 127}}}, {{{Sing "hello"}}}, {{{Sing "this also}}}}, are all 31 31 singleton types. The intuition is that the only inhabitant of `Sing n` is the value `n`. Notice 32 32 that `Sing` has a ''polymorphic kind'' because sometimes we apply it to numbers (which are of … … 47 47 So, if we apply it to a value of type `Sing 3` we get the ''number'' `3`, but, 48 48 if we apply it to a value of type `Sing "hello"` we would get the ''string'' `"hello"`. 49 50 So, how do we make values of type `Sing n` in the first place? This is done with 51 a the special overloaded constant `sing`: 52 {{{ 53 class SingI a where 54 sing :: Sing a 55 56  Builtin 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" ... 60 // ... etc. 61 }}} 49 62 50 63