[Haskell] Mixing monadic and non-monadic functions

[Thomas Jäger]

Hello,

I haven't followed this discussion very closely, but in case you want to
play with this sort of thing, you can check out the code from my
TMR-Article
http://www.haskell.org/tmrwiki/FunWithLinearImplicitParameters

Despite the wacky implementation it is actually surprisingly reliable,
modulo some (linear) implicit parameter quirks.

The [[1,2,3,4]] vs. [[1],[2],[3],[4]] ambiguity is resolved using the
same method as the borrow/<- proposal (by a function called `reflect');
and the function `reify' is corresponding to the enclosing do. A notable
difference is that my implementation always shows the information
whether a specific expression is a `monadic' one in the type. E.g.

*Reflection> reify [1,2,3,4] :: [[Int]]
[[1,2,3,4]]
*Reflection> [reify 1, reify 2,reify 3,reify 4] :: [[Int]]
[[1],[2],[3],[4]]
*Reflection> reify [reflect [1,2], reflect [3,4]] :: [[Int]]
[[1,3],[1,4],[2,3],[2,4]]

Here [reflect [1,2], reflect [3,4]] has the type Monadic [] [Int] (where
Monadic is a type synonym involving linear implicit parameters...).


However, when doing such a thing, one must decide for an evaluation
order. Because of the way it is implemented, my code uses Haskell's lazy
strategy but that makes reasoning about the resulting programs very hard
(though I believe it can be made precise):

*Reflection> reify (tail $ [reflect [1,2],3,4]) :: [[Int]]
[[3,4]]
*Reflection> reify (tail $!! [reflect [1,2],3,4]) :: [[Int]]
[[3,4],[3,4]]

(here, $!! is deepSeq'ed application)

An eager strategy might be less obscure, but suffers from the problems
described by Ben. It should also be noted that a Call-By-Name-like
strategy can be emulated with appropriate types, as in:

*Reflection> reify (let x :: Monadic [] Int; x = reflect [1,2] in [x,x])
[[1,1],[1,2],[2,1],[2,2]]
*Reflection> reify (let x :: Int; x = reflect [1,2] in [x,x])
[[1,1],[2,2]]

Of course, in case of no explicit type signature, the monomorphism
restriction plays an infamous role and the behavior depends on the flag
-fno-monomorphism-restriction.


Thomas