safelookup.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality
import Unsafe.Coerce

data Dict (ks :: [(Symbol,*)]) where
    Empty :: Dict '[]
    Ins   :: KnownSymbol k => Elem k t -> Dict ks -> Dict ('(k,t) ': ks)

data Elem (a :: Symbol) t = Elem t

type family Or (a :: Bool) (b :: Bool) :: Bool where
    Or False False = False
    Or a     b     = True

type family Fst (a :: (k, l)) :: k
type instance Fst '(k, l) = k

type family HasKey (k :: Symbol) (ks :: [(Symbol, *)]) :: Bool
type instance HasKey k '[] = 'False
type instance HasKey k (e ': ks) = Or (k == Fst e) (HasKey k ks)

type family If (b :: Bool) (t :: k) (f :: k) :: k
type instance If 'True  t f = t
type instance If 'False t f = f

type family Value (k :: Symbol) (ks :: [(Symbol, *)]) :: *
type instance Value k ('(l, v) ': ks) = If (k == l) v (Value k ks)

data W = forall a. W a

sdictToDict :: Dict ks -> [(String, W)]
sdictToDict Empty = []
sdictToDict ((Elem v :: Elem k v) `Ins` l) = (symbolVal (Proxy :: Proxy k), W v) : sdictToDict l

dLookup :: forall k ks. (HasKey k ks ~ True, KnownSymbol k)
        => Proxy (k :: Symbol) -> Dict ks -> Value k ks
dLookup _ d = case maybe undefined id . lookup (symbolVal (Proxy :: Proxy k)) $ sdictToDict d of
    W a -> unsafeCoerce a

dict :: Dict ['("dog", String), '("cat", Int)]
dict = 
    Ins (Elem "bowwow" :: Elem "dog" String) $
    Ins (Elem 222      :: Elem "cat" Int) $ 
    Empty

safelookup2.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}

import GHC.TypeLits
import Data.Proxy
import Unsafe.Coerce

data Dict (ks :: [(Symbol,*)]) where
    Empty :: Dict '[]
    Ins   :: KnownSymbol k => Elem k t -> Dict ks -> Dict ('(k,t) ': ks)

data Elem (a :: Symbol) t = Elem t

type family Lookup (key :: Symbol) (ks :: [(Symbol,*)]) where
  Lookup key ('(key, v) ': ks) = v
  Lookup key ('(k, v) ': ks) = Lookup key ks

class Member (key :: Symbol) (ks :: [(Symbol,*)]) where
  dLookup :: Proxy key -> Dict ks -> Lookup key ks

instance Member key ('(key,v) ': d) where
    dLookup _ (Elem v `Ins` _) = v

instance Member key d => Member key ('(key',v) ': d) where
    dLookup p (_ `Ins` ks) = unsafeCoerce $ dLookup p ks

dict :: Dict ['("dog", String), '("cat", Int)]
dict = 
    Ins (Elem "bowwow" :: Elem "dog" String) $
    Ins (Elem 222      :: Elem "cat" Int) $ 
    Empty

safelookup3.hs

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits(Symbol)
import Data.Proxy

data Dict (ks :: [(Symbol,*)]) where
    Empty :: Dict '[]
    Ins   :: Elem k t -> Dict ks -> Dict ('(k,t) ': ks)

data Elem (a :: Symbol) t = Elem t

class Member (key :: Symbol) (ks :: [(Symbol,*)]) out | key ks -> out where
  dLookup :: Proxy key -> Dict ks -> out

-- keyがマッチしたとき
instance Member key ('(key,v) ': d) v where
    dLookup _ (Elem v `Ins` _) = v

-- マッチしないとき
instance Member key d out => Member key ('(key',v) ': d) out where
    dLookup p (_ `Ins` ks) = dLookup p ks

dict :: Dict ['("dog", String), '("cat", Int)]
dict = 
    Ins (Elem "bowwow" :: Elem "dog" String) $
    Ins (Elem 222      :: Elem "cat" Int) $ 
    Empty