IndTypesPerfMerge.hs 5.02 KB
Newer Older
1
{-# LANGUAGE EmptyDataDecls, TypeFamilies, UndecidableInstances,
2
             ScopedTypeVariables, TypeOperators,
3
             FlexibleInstances, NoMonomorphismRestriction,
4
             MultiParamTypeClasses, FlexibleContexts #-}
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
module IndTypesPerfMerge where

data a :* b = a :* b
infixr 6 :*

data TRUE
data FALSE
data Zero
data Succ a

type family Equals m n
type instance Equals Zero Zero = TRUE
type instance Equals (Succ a) Zero = FALSE
type instance Equals Zero (Succ a) = FALSE
type instance Equals (Succ a) (Succ b) = Equals a b

type family LessThan m n
type instance LessThan Zero Zero = FALSE
type instance LessThan (Succ n) Zero = FALSE
type instance LessThan Zero (Succ n) = TRUE
type instance LessThan (Succ m) (Succ n) = LessThan m n

newtype Tagged n a = Tagged a deriving (Show,Eq)

type family Cond p a b

type instance Cond TRUE a b = a
type instance Cond FALSE a b = b

class Merger a where
    type Merged a
    type UnmergedLeft a
    type UnmergedRight a
    mkMerge :: a -> UnmergedLeft a -> UnmergedRight a -> Merged a

class Mergeable a b where
    type MergerType a b
    merger :: a -> b -> MergerType a b

44 45 46 47 48 49 50 51
{-
merge ::
    forall a b.
    (Merger (MergerType a b), Mergeable a b,
     UnmergedLeft (MergerType a b) ~ a,
     UnmergedRight (MergerType a b) ~ b) =>
    a -> b -> Merged (MergerType a b)
-}
52 53
merge x y = mkMerge (merger x y) x y

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 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97

{- ------------- NASTY TYPE FOR merge -----------------
   -- See Trac #11408

   x:tx, y:ty
   mkMerge @ gamma
   merger @ alpha beta
   merge :: tx -> ty -> tr

Constraints generated:
   gamma ~ MergerType alpha beta
   UnmergedLeft gamma ~ tx
   UnmergedRight gamma ~ ty
   alpha ~ tx
   beta ~ ty
   tr ~ Merged gamma
   Mergeable tx ty
   Merger gamma

One solve path:
  gamma := t
  tx := alpha := UnmergedLeft t
  ty := beta  := UnmergedRight t

  Mergeable (UnmergedLeft t) (UnmergedRight t)
  Merger t
  t ~ MergerType (UnmergedLeft t) (UnmergedRight t)

  LEADS TO AMBIGUOUS TYPE

Another solve path:
  tx := alpha
  ty := beta
  gamma := MergerType alpha beta

  UnmergedLeft (MergerType alpah beta) ~ alpha
  UnmergedRight (MergerType alpah beta) ~ beta
  Merger (MergerType alpha beta)
  Mergeable alpha beta

  LEADS TO NON-AMBIGUOUS TYPE
---------------  -}


98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
data TakeRight a
data TakeLeft a
data DiscardRightHead a b c d
data LeftHeadFirst a b c d
data RightHeadFirst a b c d
data EndMerge

instance Mergeable () () where
    type MergerType () () = EndMerge
    merger = undefined

instance Mergeable () (a :* b) where
    type MergerType () (a :* b) = TakeRight (a :* b)
    merger = undefined
instance Mergeable (a :* b) () where
    type MergerType (a :* b) () = TakeLeft (a :* b)
    merger = undefined

instance Mergeable (Tagged m a :* t1) (Tagged n b :* t2) where
    type MergerType (Tagged m a :* t1) (Tagged n b :* t2) =
        Cond (Equals m n) (DiscardRightHead (Tagged m a) t1 (Tagged n b) t2)
           (Cond (LessThan m n) (LeftHeadFirst (Tagged m a) t1 (Tagged n b) t2)
               (RightHeadFirst (Tagged m a ) t1 (Tagged n b) t2))
    merger = undefined

instance Merger EndMerge where
    type Merged EndMerge = ()
    type UnmergedLeft EndMerge = ()
    type UnmergedRight EndMerge = ()
    mkMerge _ () () = ()

instance Merger (TakeRight a) where
    type Merged (TakeRight a) = a
    type UnmergedLeft (TakeRight a) = ()
    type UnmergedRight (TakeRight a) = a
    mkMerge _ () a = a

instance Merger (TakeLeft a) where
    type Merged (TakeLeft a) = a
    type UnmergedLeft (TakeLeft a) = a
    type UnmergedRight (TakeLeft a) = ()
    mkMerge _ a () = a

instance
    (Mergeable t1 t2,
     Merger (MergerType t1 t2),
     t1 ~ UnmergedLeft (MergerType t1 t2),
     t2 ~ UnmergedRight (MergerType t1 t2)) =>
    Merger (DiscardRightHead h1 t1 h2 t2) where
    type Merged (DiscardRightHead h1 t1 h2 t2) = h1 :* Merged (MergerType t1 t2)
    type UnmergedLeft (DiscardRightHead h1 t1 h2 t2) = h1 :* t1
    type UnmergedRight (DiscardRightHead h1 t1 h2 t2) = h2 :* t2
    mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 t2) t1 t2

instance
    (Mergeable t1 (h2 :* t2),
     Merger (MergerType t1 (h2 :* t2)),
     t1 ~ UnmergedLeft (MergerType t1 (h2 :* t2)),
     (h2 :* t2) ~ UnmergedRight (MergerType t1 (h2 :* t2))) =>
    Merger (LeftHeadFirst h1 t1 h2 t2) where
    type Merged (LeftHeadFirst h1 t1 h2 t2) = h1 :* Merged (MergerType t1 (h2 :* t2))
    type UnmergedLeft (LeftHeadFirst h1 t1 h2 t2) = h1 :* t1
    type UnmergedRight (LeftHeadFirst h1 t1 h2 t2) = h2 :* t2
    mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 (h2 :* t2)) t1 (h2 :* t2)

instance
    (Mergeable (h1 :* t1) t2,
     Merger (MergerType (h1 :* t1) t2),
     (h1 :* t1) ~ UnmergedLeft (MergerType (h1 :* t1) t2),
     t2 ~ UnmergedRight (MergerType (h1 :* t1) t2)) =>
    Merger (RightHeadFirst h1 t1 h2 t2) where
    type Merged (RightHeadFirst h1 t1 h2 t2) = h2 :* Merged (MergerType (h1 :* t1) t2)
    type UnmergedLeft (RightHeadFirst h1 t1 h2 t2) = h1 :* t1
    type UnmergedRight (RightHeadFirst h1 t1 h2 t2) = h2 :* t2
172
    mkMerge _ (h1 :* t1) (h2 :* t2) = h2 :* mkMerge (merger (h1 :* t1) t2) (h1 :* t1) t2