[Haskell-cafe] How to convert a list to a vector encoding its
length in its type?
Daniel Peebles
pumpkingod at gmail.com
Fri Aug 21 14:16:24 EDT 2009
Just to expand on David's higher-order function for the original
Vector type, we can do:
data AnyVec a where
AnyVec :: Vec a n -> AnyVec a
listToVec :: [a] -> AnyVec a
listToVec = worker AnyVec
worker :: (forall n. Nat n => Vec a n -> t) -> [a] -> t
worker f [] = f Nil
worker f (x:xs) = worker (f . (Cons x)) xs
and have it behave as you'd expect. Note that in a sense this is
"forgetful" of the original length of the list.
Dan
On Fri, Aug 21, 2009 at 2:03 PM, David Menendez<dave at zednenem.com> wrote:
> On Fri, Aug 21, 2009 at 1:03 PM, Jason Dagit<dagit at codersbase.com> wrote:
>>
>> Even with a type class for our type level numbers I'm at a loss. I
>> just don't understand how to convert an arbitrary int into an
>> arbitrary but fixed type. Perhaps someone else on the list knows. I
>> would like to know, if it's possible, how to do it.
>>
>> toPeano :: Nat n => Int -> n
>
> The problem is that the parameter, n, is part of the input to toPeano,
> but you need it to be part of the output. To rephrase slightly, you
> have
>
> toPeano :: forall n. (Nat n) => Int -> n
>
> but you need,
>
> toPeano :: Int -> exists n. (Nat n) => n
>
> which states that toPeano determines the type of its return value. In
> Haskell, you can encode this with an existential data type,
>
> data SomeNat where SomeNat :: (Nat n) => n -> SomeNat
> toPeano :: Int -> SomeNat
>
> or, equivalently, by using a higher-order function.
>
> toPeano :: Int -> (forall n. Nat n => n -> t) -> t
>
> --
> Dave Menendez <dave at zednenem.com>
> <http://www.eyrie.org/~zednenem/>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
More information about the Haskell-Cafe
mailing list