Polymorphic lists...

[oleg at pobox.com]

Hello, Ralf!

> In fact, he mentions that values can be retrieved by either type or
> index, while only the former is discussed in detail, if I am right. To
> me it seems, he would also need to end up using dependant-type
> encoding of naturals, say data Zero ... and data Succ ..., for
> look-up. If I am still right, then his operator type_index is
> underspecified because it returns a plain Int, but Int could be
> replaced by dependant-type Naturals.

Indexing of types by regular integers was discussed in 
	http://www.mail-archive.com/haskell@haskell.org/msg13163.html
which was a response to your comments. I hope you saw them. The topic
was encoding and storing of values of _polymorphic_ datatypes.

However, the following is a more succinct realization of a polymorphic
list. Retrieval is done by ordinary _integers_. The list behaves
roughly as a regular list. Although we use the type of a value to
obtain the integral index, and we use the integral index to fetch the
value.

>{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances #-}
>
> module Foo where
>
> class (Show a) => TH a b where
>     idx:: a -> b -> Int
>     alter:: a -> b -> b
>     tke:: a -> b -> (forall u v. TH u v => u -> v -> w) -> w
>
> instance (Show a) => TH a (a,x) where
>    idx x y = 0
>    alter x (_,y) = (x,y)
>
> instance (TH a c) => TH a (b,c) where
>    idx x y = 1 + idx x (undefined::c)
>    alter x (h,t) = (h,alter x t)
>
> data W = W Int deriving Show
>
> instance (TH a (a,b), TH W b) => TH W (a,b) where
>     tke (W 0) th@(h,t) f = f h th
>     tke (W n) (h,t) f = tke (W$ n-1) t f
>
> instance TH W () where
>     tke _ _ _ = error "Not found"

That's it. Class Show is for expository purposes, so we can print what
we've got.

The following is to enable us to store functional values

> instance Show (a->b) where show _ = "<fn>"

Here's the initial heap

> infixr 5 &+
>
> a &+ b = (a,b)
>
> th1 = (1::Int) &+ 'x' &+ (Just True) &+ () &+ [1.0::Float]
>       &+ (\(c::Char) -> True)
>       &+ () -- just to mark the end of it

Now the fun begins:

*Foo> idx 'a' th1
1
*Foo> idx [2.0::Float] th1
4
*Foo> idx (=='c') th1
5

We can use a functional type as an index. We can fetch things too:

*Foo> tke (W 0) th1 (const.show)
"1"
*Foo> tke (W 1) th1 (const.show)
"'x'"
*Foo> tke (W 4) th1 (const.show)
"[1.0]"
*Foo> tke (W 5) th1 (const.show)
"<fn>"

We can store and retrieve things

*Foo> tke (W 4) (alter [1.0::Float, 2.0::Float] th1) (const.show)
"[1.0,2.0]"

Right fold can be done along the lines of tke. Only a type like W
will hold our accumulator.