## 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 ret <- var (xs.head) 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?

## 7 Comments:

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

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

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.

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

{-# LANGUAGE GADTs #-}

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)

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

{-# LANGUAGE GADTs #-}

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)

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.

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

Post a Comment

<< Home