[Haskell-cafe] How to convert a list to a vector encoding its
length in its type?
Bas van Dijk
v.dijk.bas at gmail.com
Mon Aug 24 19:24:48 EDT 2009
On Tue, Aug 25, 2009 at 12:07 AM, Ryan Ingram<ryani.spam at 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
More information about the Haskell-Cafe
mailing list