VinylRecords/Vinyl — pull request #27 by conklech (2013-11-28 03:38:16+00:00)
Title: Implement "lazy" records using type families

Because `Rec` is a GADT, it cannot be used inside a lazy (~) pattern. You can't write a pattern like `~(x :& y :& RNil)`. Therefore certain recursive programs which require laziness cannot be written using Rec. This patch adds an alternative implementation, `LazyRec`, using type families to avoid that shortcoming.

The main downside to `LazyRec` is that recursive functions are less convenient to write. You can't just pattern match on `RNil`/`(:&)`, because `RNilL` and `(:&~)` are constructors of different types. You have to use type classes, as with `ToRec` and `FromRec`.

A few implementation notes:

- Almost everything is closely paraphrased from the existing implementation.
- The altered `Elem'` witness is needed so that `go` in `rLensL'` has evidence that `y ~ (sy ::: t)` each time it recurses through a `There'`. (GHC threw an impressively enormous list of errors at me when I first tried to implement `rLensL'`.)
- We need `UndecidableInstances` to write `instance (y ~ (sy ::: t), Implicit (Elem' x xs)) => Implicit (Elem' x (y ': xs))`. I don't know if that's a bad thing.
- I have not evaluated performance at all.
- In the class instances, I threw in `~` and `_` everywhere. I haven't really thought through what should be pattern-matched.

Here's a contrived example where `Rec` can't be used because the lazy pattern is necessary. (You need `RecursiveDo`.)

type F = '["x" ::: String, "y" ::: String]
f1 :: LazyRec F Identity -> IO (LazyRec F Identity)
f1 ~(Identity x :&~ _) = do
putStrLn "f1"
return $ Identity ('x' : x) :&~ Identity "b" :&~ RNilL

f2 :: LazyRec F Identity -> IO (LazyRec F Identity)
f2 ~(_ :&~ Identity y :&~ _) = do
putStrLn "f2"
return $ Identity "a" :&~ Identity ('y' : y) :&~ RNilL

testFix :: IO (LazyRec F Identity, LazyRec F Identity)
testFix = mdo
x <- f1 y -- Reversing these two lines will change what's printed to stdout,
y <- f2 x -- but the resulting tuple will be the same.
return (x, y)

Without the lazy patterns, this will hang.