gdiffHaskell library, even for use cases it was not originally designed for.
This is mostly a brain dump of some approaches I have learnt while tinkering and trying to solve certain problems.
diff: Eelco Lempsink writes in the conclusion of his 2010 thesis «Furthermore, we can not encode polymorphic datatypes such as lists, but need to write specific encodings for each type we want to include». In the library documentation he says «It might require another master thesis project to solve this». However in the last days I developed a trick, which does allow me to describe polymorphic data types, such as
Maybe a. I just needed to add these lines:
in the family GADT:
ListNil :: List Fam as → Fam a as → Fam [a] Nilthen define a
ListCons :: List Fam as → Fam a as → Fam [a] (a `Cons` [a] `Cons` Nil)
instance Type Fam a ⇒ Type Fam [a] where
constructors = head [Concr (ListNil cc) | Concr cc Concr cc ← constructors] : [head [Concr (ListCons cc) | Concr cc ← constructors]]
What is this doing? It picks two random constructors from the underlying data type and wraps them with
ListCons. We usually ignore what is wrapped, with one exception: in
decEqone needs to ensure that the constructors' arguments are compared too, otherwise one cannot finish the type equality proof.
2) Non-moving pairs: In the usual textual
diffalgorithm the lines may move around a bit to make room for insertions, etc. This is normally the case for
gdifftoo. I have seen
gdiffreusing values (with
Cpy) when comparing
(False, True). But sometimes this is not desired at all. I figured out that "inlining" the leaves into the pair's description (i.e. instead of
(a `Cons` b `Cons` Nil)writing
appendListon the field decompositions of
bdoes the trick.
3) Location types: I found a way to equip
Abstrconstructor descriptors with type class dictionaries. It is similar to the lifting approach shown under 1), but much more involved.
The idea is to wrap a location-aware descriptor with a descriptor that is location-blind, i.e. that hides the location parameter:
Loc' :: KnownNat n ⇒ Fam (Loc n Bool) …
Then we need the wrapper:
Hidden' :: KnownNat n ⇒ Fam (Loc n Bool) ts → Fam (Hidden Loc) ts
Typeinstance for the latter is tricky, as
Abstralone has no provision for dodging the class dictionary into
Hidden', so I had to write a
locAwaresmart constructor to syphon it through the
This also stressed the compiler to its limits in the advanced
PolyKind-ed approach I needed, so I filed a GHC bug #9725. There is also some code showing how the
Hidden Locis unwrapped and the dictionary-passing functions is installed into the
4) Monadic actions coming out of
patch: Here another wrapping approach is needed, but this time we need a sum type for
patchso that we can enter with a pure value at the
Leftand obtain a
Rightaction back. This is the most involved approach. I can probably blog another time about it.