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.