public
Created

Type Level Associative Array

  • Download Gist
gistfile1.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
{-# 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

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.