This is without class :-)

{-# LANGUAGE TypeFamilies, ExistentialQuantification, FlexibleContexts #-}
import Prelude hiding (lookup)
import Data.Typeable

type family Value a :: *
   
data Assoc = forall a . (Typeable (Value a), Typeable a) => Assoc a (Value a)

insert :: (Typeable (Value a), Typeable a) => a -> Value a -> [Assoc] -> [Assoc]
insert k v = (Assoc k v :)

lookup :: (Typeable (Value a), Typeable a, Eq a) => a -> [Assoc] -> Value a
lookup k [] = error "noassoc"
lookup k ((Assoc k' v):xs) = case cast k' of
        Nothing -> lookup k xs
        Just k'' -> if k'' == k then case cast v of
                Nothing -> error "nocast"
                Just v' -> v'
            else lookup k xs

*Main> type instance Value Integer  = Char
*Main> type instance Value Int = String
*Main> let u = insert (1::Integer) 'c' $ insert (1::Int) "ciao" []
*Main> lookup (1 :: Integer)  u
'c'
*Main> lookup (1 :: Int)  u
"ciao"
*Main>

Regards
paolino

2012/8/1 Paolino <paolo.veronelli@gmail.com>

Hello, I made some trial and error with ghci to make it happy. I'm not really sure this has the type safety you asked.

{-# LANGUAGE TypeFamilies, ExistentialQuantification, FlexibleContexts #-}

import Prelude hiding (lookup)
import Data.Typeable

class Typeable a => Key a where
    type Value a :: *
   
data Assoc = forall a . (Typeable (Value a),Key a) => Assoc a (Value a)

insert :: (Typeable (Value a), Key a) => a -> Value a -> [Assoc] -> [Assoc]
insert k v = (Assoc k v :)

lookup :: (Typeable (Value a), Eq a, Key a) => a -> [Assoc] -> Value a
lookup k [] = error "noassoc"
lookup k ((Assoc k' v):xs) = case cast k' of
        Nothing -> lookup k xs
        Just k'' -> if k'' == k then case cast v of
                Nothing -> error "nocast"
                Just v' -> v'
            else lookup k xs

I've tried without the typeclass with no luck.
For some reasons

type family Key a :: *
type family Value a :: *

and adding Typeable (Key a) to the contexts and Key 'a' in place of 'a' leads to a lot of type errors.
Maybe it's possible with more help.

Hope I got it right.

Regards
paolino


2012/7/31 Alexander Foremny <alexanderforemny@gmail.com>
Hello list,

I am currently thinking that a problem of mine would best be solved if
there was a Map-like data structure in which the value returned is
parametrized over the lookup type.

I wonder is this makes sense and if such a data structure exists or if
it could be created while still being well typed. I essentially want
to statically define a scope of Key values and dynamically define a
list of keys.

> -- Scope of possible keys.
> type Label = String
> data Key a where
>     KeyStr :: Label -> Key String
>     KeyInt :: Label -> Key Int
>     KeyChoice :: Label -> [a] -> Key a

> -- Some key values, to be extended at runtime.
> strKey "Some String"
> strKey' "Another String"
> intKey "Some integer"
> choiceKey "Chose one" [ "a", "b", "c" ] :: KeyChoice String

Now I need a data structure to possibly associate a value to the key.

> data MapG = ...
> type Value a = a
> insert :: Key a -> Value a -> MapG Key Value -> MapG Key Value
> lookup :: Key a -> MapG Key Value -> Maybe (Value a)

I tried implementing this with multiple Map k a's. I tried adding a
phantom type on some storage type of to implement KeyChoice as of type
Key Int, but I ran into troubles with this approach. I wonder if
Dynamic or Type Families could achieve this, but I am quite at a loss
and would like to hear your opinion.

I did try to search for this a bit, but I don't quite know how to
phrase my problem. I'd like to apologize in advance if this question
has been asked already.

Regards,
Alexander Foremny

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe