--- /dev/null
+{-# LANGUAGE
+ EmptyDataDecls,
+ TypeFamilies,
+ TypeOperators,
+ UndecidableInstances
+ #-}
+module Types.Data.Map
+ ( Map
+
+ , Null
+ , Size
+ , Lookup
+ , LookupAssoc
+ , Member
+ , NotMember
+ , Find
+ , FindWithDefault
+
+ , Empty
+ , Singleton
+
+ , Insert
+ )
+ where
+
+import Types.Data.Bool
+import Types.Data.List hiding (Null)
+import Types.Data.Maybe
+import Types.Data.Num
+import Types.Data.Ord
+
+data Tip
+data Bin size key value left right
+
+class Map m
+instance Map Tip
+instance Map (Bin s k v l r)
+
+-- Null
+type family Null m
+type instance Null Tip = True
+type instance Null (Bin s k v l r) = False
+
+-- Size
+type family Size m
+type instance Size Tip = D0
+type instance Size (Bin s k v l r) = s
+
+-- Lookup
+type family Lookup k m
+type instance Lookup k Tip = Nothing
+type instance Lookup k (Bin s k' v l r)
+ = If (IsLT (Compare k k'))
+ (Lookup k l)
+ (If (IsGT (Compare k k'))
+ (Lookup k r)
+ (Just v))
+
+-- LookupAssoc
+type family LookupAssoc k m
+type instance LookupAssoc k Tip = Nothing
+type instance LookupAssoc k (Bin s k' v l r)
+ = If (IsLT (Compare k k'))
+ (LookupAssoc k l)
+ (If (IsGT (Compare k k'))
+ (LookupAssoc k r)
+ (Just (Cons k v)))
+
+-- Member
+type Member k m = IsJust (Lookup k m)
+
+-- NotMember
+type NotMember k m = Not (Member k m)
+
+-- Find
+type Find k m = FromJust (Lookup k m)
+
+-- FindWithDefault
+type FindWithDefault a k m
+ = FromMaybe a (Lookup k m)
+
+-- Empty
+type Empty = Tip
+
+-- Singleton
+type Singleton k v = Bin D1 k v Tip Tip
+
+-- Insert
+type family Insert k v m
+type instance Insert k v Tip = Singleton k v
+type instance Insert k v (Bin s k' v' l r)
+ = If (IsLT (Compare k k'))
+ (Balance k' v' (Insert k v l) r)
+ (If (IsGT (Compare k k'))
+ (Balance k' v' l (Insert k v r))
+ (Bin s k v l r))
+
+-- Balance
+type Delta = D5
+type Ratio = D2
+
+type Balance k v l r
+ = If (Size l :+: Size r :<: 1)
+ (Bin (Size l :+: Size r :+: D1) k v l r)
+ (If (Size r :>=: Delta :*: Size l)
+ (RotateL k v l r)
+ (If (Size l :>=: Delta :*: Size r)
+ (RotateR k v l r)
+ (Bin (Size l :+: Size r :+: D1) k v l r)))
+
+-- Rotate
+type family RotateL k v l r
+type instance RotateL k v l (Bin s k' v' l' r')
+ = If (Size l' :<: Ratio :*: Size r')
+ (SingleL k v l (Bin s k' v' l' r'))
+ (DoubleL k v l (Bin s k' v' l' r'))
+
+type family RotateR k v l r
+type instance RotateR k v (Bin s k' v' l' r') r
+ = If (Size r' :<: Ratio :*: Size l')
+ (SingleR k v (Bin s k' v' l' r') r)
+ (DoubleR k v (Bin s k' v' l' r') r)
+
+-- Rotations
+type family SingleL k v l r
+type instance SingleL k v l (Bin s k' v' l' r')
+ = Bin' k' v' (Bin' k v l l') r'
+
+type family SingleR k v l r
+type instance SingleR k v (Bin s k' v' l r) r'
+ = Bin' k' v' l (Bin' k v r r')
+
+type family DoubleL k v l r
+type instance DoubleL k v l (Bin s k' v' (Bin s' k'' v'' l' r) r')
+ = Bin' k'' v'' (Bin' k v l l') (Bin' k' v' r r')
+
+type family DoubleR k v l r
+type instance DoubleR k v (Bin s k' v' l (Bin s' k'' v'' l' r)) r'
+ = Bin' k'' v'' (Bin' k' v' l l') (Bin' k v r r')
+
+-- Bin'
+type Bin' k v l r
+ = Bin (Size l :+: Size r :+: D1) k v l r
+