Skip to content

Instantly share code, notes, and snippets.

@jfischoff
Created November 7, 2012 20:41
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jfischoff/4034291 to your computer and use it in GitHub Desktop.
Save jfischoff/4034291 to your computer and use it in GitHub Desktop.
Type Level Associative Array
{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies,
GADTs, TypeOperators, RankNTypes, FlexibleContexts, UndecidableInstances,
FlexibleInstances, ScopedTypeVariables, MultiParamTypeClasses,
OverlappingInstances, TemplateHaskell #-}
module Oxymoron.Regions.TAssociativeArray where
import Data.Singletons
singletons [d| data AssocArray a b = AssocArray [(a, b)] |]
type instance ('AssocArray xs) :==: ('AssocArray ys) =
If ((xs :==: '[ ]) :&&: (ys :==: '[ ]))
True
(If (xs :==: '[ ]) False (
If (ys :==: '[ ])
False
(xs :==: (Reorder ys xs))
))
type instance '(a, b) :==: '(x, y) = (a :==: x) :&&: (b :==: y)
type family Fst (x :: (a,b)) :: a
type instance Fst '(a,b) = a
type family Snd (x :: (a,b)) :: b
type instance Snd '(a,b) = b
-- remove a DimSpec from a list, if it's in the list;
-- returns the new list and possibly the extracted element
type family Extract (s :: k) (lst :: [k]) :: ([k], Maybe k)
type instance Extract s '[] = '( '[], Nothing)
type instance Extract s (h ': t) =
If (s :==: h)
'(t, Just h)
'(h ': Fst (Extract s t), Snd (Extract s t))
-- reorder 'a' in the order defined by 'b'.
type family Reorder (a :: [k]) (b :: [k]) :: [k]
type instance Reorder x '[] = x
type instance Reorder x (h ': t) = Reorder' (Extract h x) t
type family Reorder' (scrut :: ([k], Maybe k))
(t :: [k])
:: [k]
type instance Reorder' '(lst, Nothing) t = Reorder lst t
type instance Reorder' '(lst, Just elt) t = elt ': (Reorder lst t)
singletons [d| data TestValue = Test1
| Test2
| Test3
deriving(Eq, Show)
data TestKey = Key1
| Key2
| Key3
deriving(Eq, Show)
|]
test :: ((a :==: b) ~ True) => Sing (a :: AssocArray k v) -> Sing (b :: AssocArray k v) -> Int
test = undefined
testA :: Sing ('AssocArray '[ '( 'Key1, 'Test3 ),
'( 'Key2, 'Test2 )])
testA = undefined
testB :: Sing ('AssocArray '[ '( 'Key2, 'Test2),
'( 'Key1, 'Test3)])
testB = undefined
testC :: Sing ('AssocArray '[ '( 'Key2, 'Test3) ])
testC = undefined
-- Order is different but it still compiles
test1 = test testA testB
-- this won't compile
--test2 = test testA testC
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment