## Impredicative polymorphism, a use case

In a recent question on stackoverflow I made a comment about how Haskell can be considered a good imperative language because you can define abstractions to make it convenient. When I was going to make my point by implementing a simple example of it I found that what I wanted to do no longer works in ghc-7.0.4. Here's a simple example of what I wanted to do (which works in ghc-6.12.3). It's a simple library that makes Haskell code look a bit like Python.

```{-# LANGUAGE ExtendedDefaultRules, TupleSections #-}
module Main where
import qualified Prelude
import Boa

last_elt(xs) = def \$: do
assert xs "Empty list"
lst <- var xs              -- Create a new variable, lst
while lst \$: do
ret #= lst.head        -- Assign variable ret
lst #= lst.tail
return ret

first_elt(xs) = def \$: do
l <- var xs
l.reverse                  -- Destructive reverse
return (last_elt(l))

factorial(n) = def \$: do
assert (n<=0) "Negative factorial"
ret <- var 1
i <- var n
while i \$: do
ret *= i
i -= 1
return ret

test = def \$: do
print "Hello"
print ("factorial 10 =", factorial(10))

main = do
test
l <- varc [1, 2, 3]
print ("first and last:",)
print (first_elt(l),)
print (last_elt(l))
```

On the whole it's pretty boring, except for one thing. In imperative languages there is (usually) a disctinction between l-values and r-values. An l-value represent a variable, i.e., something that can be assigned, whereas an r-value is simply a value. So in Python, in the statement x = x + 1 the x on the left is an l-value (it's being assigned), whereas on the right it's an r-value. You can use the same notation for both in most imperative languages. If you want to do the same in Haskell you have (at least) two choices. First you can unify the concepts of l-value and r-value and have a runtime test that you only try to assign variables. So, e.g., 5 = x would type check but have a runtime failure. I will not dwell further on this since it's not very Haskelly.
Instead, we want to have l-values and r-values being statically type checked. Here's the interesting bit of the types for a simple example.
` `
```data LValue a
data RValue a
instance (Num a) => Num (RValue a)

class LR lr
instance LR RValue
instance LR LValue

var :: RValue a -> IO (forall lr . (LR lr) => lr a)
(#=) :: LValue a -> RValue a -> IO ()

foo = do
x <- var 42
x #= x + 1
```

We have two type constructors LValue and RValue representing l-values and r-values of some type a. The r-values is an instance of Num. Furthermore, the class LR where the type is either LValue or RValue.
The var function creates a new variable given a value. The return type of var is the interesting part. It says that the return value is polymorphic; it can be used either as an l-value or as r-value. Just as we want.
The assignment operator, (#=), takes an l-value, an r-value, and returns nothing.

So in the example we expect x to have type forall lr . (LR lr) => lr a, in which case the assignment will type check.
If we try to compile this we get
```    Illegal polymorphic or qualified type:
forall (lr :: * -> *). LR lr => lr a
Perhaps you intended to use -XImpredicativeTypes
In the type signature for `var':
var :: RValue a -> IO (forall lr. LR lr => lr a)
```

The problem is that universal quantification is not normally allowed as the argument to a type constructor. This requires the impredicative polymorphism extension to ghc. If we turn it on it compiles fine in ghc-6.12.3.
But, with ghc-7.0.4 we get
```    Couldn't match expected type `LValue a0'
with actual type `forall (lr :: * -> *). LR lr => lr a1'
In the first argument of `(#=)', namely `x'
In the expression: x #= x + 1
```

I can't really explain the rational behind the change in the ghc type system (Simon say it's simpler now), but I feel this has really made ghc worse for defining DSELs. When you define a DSEL you usually use the do-notation for the binding construct in the embedded language. This is the only programmable binding construct (by overloading (>>=)), so there is little choice. With the change in ghc-7 it means you can no longer make DSELs with a polymorhic binding construct (like I wanted here), because the binder seems to be monomorphic now

Please Simon, can we have polymorphic do bindings back?

Anders Kaseorg said...

You can do this without impredicative polymorphism just by adding an explicit data constructor:

newtype Var a = Var (forall lr . LR lr => lr a)
var :: RValue a -> IO (Var a)
(#=) :: LValue a -> RValue a -> IO ()

foo = do
Var x <- var 42
x #= x + 1

Saturday, July 9, 2011 at 9:30:00 PM GMT+1
augustss said...

The 'Var x' in the binder is not acceptable to me. Otherwise, yeah.

Sunday, July 10, 2011 at 1:11:00 AM GMT+1
Andy Gill said...

We used the Var x variant in Kansas Lava. We use it to encode two types of variables, Var and Reg, which have different timing semantics. Thus, turning a required annotation into a useful and required syntax.

Sunday, July 10, 2011 at 1:44:00 AM GMT+1
meteficha said...

It may be possible to do something with GADTs like the following. Seems like a nice approach to me.

import qualified Prelude as P

data LValue -- empty
data RValue -- empty

data Expr t a where
Var :: Expr LValue a
Num :: P.Double -> Expr RValue P.Double

class LR lr
instance LR RValue
instance LR LValue

var :: Expr t a -> P.IO (Expr LValue a)
(#=) :: (LR lr) => Expr LValue a -> Expr lr a -> P.IO ()
(+) :: Expr t1 P.Double -> Expr t2 P.Double -> Expr RValue P.Double

foo = do
x <- var 42
x #= (x + 1)

Sunday, July 10, 2011 at 2:17:00 PM GMT+1
meteficha said...

Actually, I think that the LR class wouldn't even be needed.

import qualified Prelude as P

data LValue -- empty
data RValue -- empty

data Expr t a where
Var :: Expr LValue a
Num :: P.Double -> Expr RValue P.Double

var :: Expr t a -> P.IO (Expr LValue a)
(#=) :: Expr LValue a -> Expr t a -> P.IO ()
(+) :: Expr t1 P.Double -> Expr t2 P.Double -> Expr RValue P.Double

foo = do
x <- var 42
x #= (x + 1)

Sunday, July 10, 2011 at 2:18:00 PM GMT+1
Robert said...

Did you tried adding {-# LANGUAGE NoMonoLocalBinds #-} AFTER switching on all other extensions? As mentioned here, local bindings are monomorphic by default now, unless you turn polymorphic bindings on.

Sunday, July 10, 2011 at 3:32:00 PM GMT+1
Unknown said...

Sorry for posting it here, but I was unable to contact you by the only email I found from Chalmers.

I was wondering if you possibly have a copy of your paper "Compiling pattern matching", which I would like to read, but am unable to locate on the internet. I can be contacted by email solodon on Google's Gmail.

Thanks,
Yuriy

P.S. Your Chalmers page http://www.cs.chalmers.se/~augustss/ is not available anymore

Tuesday, August 23, 2011 at 10:00:00 PM GMT+1