AMap.hs

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, OverlappingInstances, ScopedTypeVariables #-}
import Prelude hiding ((!!))
import GHC.TypeLits

newtype Map (k :: [Nat]) v = Map [v]

empty :: Map '[] a
empty = Map []

add :: Sing k -> v -> Map ks v -> Map (k ': ks) v
add _ v (Map xs) = Map (v:xs)

class Ke (k :: Nat) (ks :: [Nat]) v where
  (!!) :: (Sing k) -> Map ks v -> v

instance Ke k (k ': ks) v where
  _ !! (Map (x:_)) = x

instance Ke k ks v => Ke k (h ': ks) v where
  k' !! (Map (_:xs)) = k' !! (Map xs :: Map ks v)

g :: Map [3, 10, 1] String
g = add (undefined :: Sing 3) "baz" $ add (undefined :: Sing 10) "bar" $ add (undefined :: Sing 1) "foo" empty

v1 = (undefined :: Sing 10) !! g
v2 = (undefined :: Sing 3) !! g
v3 = (undefined :: Sing 1) !! g
-- Type Error: v3 = (undefined :: Sing 2) !! g