Context Navigation

Changes between Version 1 and Version 2 of TypeNtas/AlternativeSingletins

v1	v2
1	1	We use a family of singleton types to related type-level naturals to runtime values.
2	2
3		In our design, we chose to provide an overloaded "smart" constructor and a polymorphic elimination construct:
	3	In our design, we chose to provide as primitive an overloaded "smart" constructor and a polymorphic elimination construct:
4	4	{{{
5	5	newtype Nat (n :: Nat) = Nat Integer
…	…
28	28	}}}
29	29
	30	We made this choice, at least in part, because it made the implementation simpler: the evidence for class {{{NatI}}} is just an integer. Note that our choice does not loose any generality because we can define the alternative design in terms of it:
30	31
	32	{{{
	33	data Nat1 (n :: Nat) = Nat
31	34
	35	nat1ToInteger :: NatI n => Nat1 n -> Integer
	36	nat1ToInteger x = natToInteger (cast nat x)
	37	where cast :: Nat n -> Nat1 n -> Nat n
	38	cast x Nat = x
	39	}}}
	40