On Mon, Aug 24, 2009 at 4:24 PM, Bas van Dijk<v.dijk....@gmail.com> wrote: > Thanks very much! I'm beginning to understand the code. > > The only thing I don't understand is why you need [witnessNat] > >> toList = ... induction (witnessNat :: n) ... >> fromList = ... induction (witnessNat :: n) ... > > However the following also works: > >> toList = ... induction (undefined :: n) ... >> fromList = ... induction (undefined :: n) ...
Yes, that's true. But because we have lazy evaluation, witnessNat never gets evaluated, so it doesn't matter :) And I prefer to keep the (undefined/error) calls, along with recursion, in my code to a minimum, since both of those can lead to _|_ and runtime errors. So, by keeping the calls to "undefined" and the use of recursion limited to "induction" and "witnessNat", I create a very small 'trusted core' of code that has to be checked carefully for errors. Other code that uses these functions are entirely safe as long as we keep those functions total and avoid explicit recursion. This is why I called out "fromJust" in my example; it's the one use of non-totality outside of the kernel. > Although 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 Yes, in my original post[1] I comment about this nicety; if I used "data" instead of "newtype" I would have implemented it as ] instance Nat Z where caseNat ~Z z _ = z ] instance Nat n => Nat (S n) where caseNat ~(S n) _ s = s n > Again, thanks very much for this! > > Do you mind if I use this code in the levmar package (soon to be > released on hackage)? No problem. I hereby release this code under the WTFPL[2], version 2 with the "no warranty" clause. -- ryan [1] Lightweight type-level dependent programming in Haskell. http://www.haskell.org/pipermail/haskell-cafe/2009-June/062690.html [2] http://sam.zoy.org/wtfpl/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe