On Tue, Aug 25, 2009 at 12:07 AM, Ryan Ingram<ryani.s...@gmail.com> wrote: > unsafeCoerce is ugly and I wouldn't count on that working properly. > > Here's a real solution: > ...
Thanks very much! I'm beginning to understand the code. The only thing I don't understand is why you need: > newtype Witness x = Witness { unWitness :: x } > witnessNat :: forall n. Nat n => n > witnessNat = theWitness where > theWitness = unWitness $ induction (undefined `asTypeOf` theWitness) > (Witness Z) (Witness . S . unWitness) I understand that 'witnessNat' is a overloaded value-level generator for Nats. So for example: 'witnessNat :: S (S (S Z))' returns the value: 'S (S (S Z))'. Then you use it in the implementation of 'toList' and 'fromList': > toList = ... induction (witnessNat :: n) ... > fromList = ... induction (witnessNat :: n) ... I guess so that 'induction' will then receive the right 'Nat' _value_. However the following also works: > toList = ... induction (undefined :: n) ... > fromList = ... induction (undefined :: n) ... Indeed, 'witnessNat' itself is implemented this way: > witnessNat = theWitness where theWitness = ... induction (undefined > `asTypeOf` theWitness) ... So the 'n' in 'induction n' is just a "type carrying parameter" i.e. it doesn't need to have a run-time representation. Al dough it looks like that a case analysis on 'n' is made at run-time in: > instance Nat n => Nat (S n) where > caseNat (S n) _ s = s n But I guess that is desugared away because 'S' is implemented as a newtype: > newtype S n = S n Indeed, when I make an actual datatype of it then 'witnessNat :: S (S (S Z))' will crash with "*** Exception: Prelude.undefined". Again, thanks very much for this! Do you mind if I use this code in the levmar package (soon to be released on hackage)? regards, Bas _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe