Existentially-quantified constructors: Hugs is fine, GHC is not?

classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Existentially-quantified constructors: Hugs is fine, GHC is not?

Otakar Smrz
Dear all,

while WinHugs (20051031) lets me match against an existentially
quantified constructor

    data ... = ... | forall b . FMap (b -> a) (Mapper s b)

    ... where FMap qf qc = stripFMap f q

the GHC compiler as well as GHCi (6.4.2 and earlier) issue an error

     My brain just exploded.
     I can't handle pattern bindings for existentially-quantified
     constructors.


Let me give the whole (non-practical) code, which is well typed and
compiles in Hugs, and then show the change I had to do to make it work
in GHC, too.

The question is why there is a difference. Am I misusing something?

The point of the complexFun below is to explore the Mapper data
structure, taking care of the :&: constructor and quickly
(transitively) skipping the FMap constructors, only accumulating and
composing the tranformation functions that these provide.

-----------------------------------------------------------

module Problem where

import Data.Map as Map hiding (map)

type Labels a = [a]

data Mapper s a = Labels a :&: Map.Map s (Mapper s a)
                 | forall b . FMap (b -> a) (Mapper s b)


stripFMap :: Ord s => (a -> c) -> Mapper s a -> Mapper s c

stripFMap k (FMap f p)  = stripFMap (k . f) p
stripFMap k x           = FMap k x


complexFun :: Ord s => (b -> a) -> Mapper s b -> s -> [a]

complexFun f c y = case c of

     FMap t q -> complexFun qf qc y

                     where FMap qf qc = stripFMap (f . t) q   -- !!!

     r :&: k  -> case Map.lookup y k of

         Just q  ->  let FMap qf qc = stripFMap f q     -- !!!
                     in case qc of

             ([] :&: _) -> complexFun qf qc y
             (xs :&: _) -> map qf xs
             _          -> error "Never matching"

         Nothing -> error "Irrelevant"

-----------------------------------------------------------

Even though GHC does not let me pattern-match on FMap, I can use a
case expression in complexFun instead -- then it compiles alright:

------

complexFun f c y = case c of

     FMap t q -> case stripFMap (f . t) q of -- !!!

         FMap qf qc -> complexFun qf qc y -- !!!
         _          -> error "No option" -- !!!

     r :&: k  -> case Map.lookup y k of

         Just q  ->  case stripFMap f q of -- !!!

           FMap qf qc -> case qc of -- !!!

             ([] :&: _) -> complexFun qf qc y
             (xs :&: _) -> map qf xs
             _          -> error "Never matching"

           _          -> error "No option" -- !!!

         Nothing -> error "Irrelevant"

------

If I wanted to make this auxiliary case on stripFMap local, there
would be a problem for both Hugs and GHC:

  Hugs: Existentially quantified variable in inferred type!
        *** Variable     : _48
        *** From pattern : FMap xf xc
        *** Result type  : (_48 -> _32,Mapper _30 _48)

  GHC: Inferred type is less polymorphic than expected
         Quantified type variable `b' is mentioned in the environment:
           qc :: Mapper s1 b (bound at Problem.hs:65:27)
           qf :: b -> a1 (bound at Problem.hs:65:23)
       When checking an existential match that binds
           xf :: b -> a
           xc :: Mapper s b
       The pattern(s) have type(s): Mapper s1 a1
       The body has type: (b -> a1, Mapper s1 b)
       In a case alternative: FMap xf xc -> (xf, xc)

------

complexFun f c y = case c of

     FMap t q -> complexFun qf qc y

                 where (qf, qc) = case stripFMap (f . t) q of  -- !!!

                         FMap xf xc -> (xf, xc)
                         _          -> error "No option"

     r :&: k  -> case Map.lookup y k of

         Just q -> let (qf, qc) = case stripFMap f q of        -- !!!

                         FMap xf xc -> (xf, xc)
                         _          -> error "No option"

                     in case qc of

             ([] :&: _) -> complexFun qf qc y
             (xs :&: _) -> map qf xs
             _          -> error "Never matching"

         Nothing -> error "Irrelevant"

------


Many thanks for your comments or advice!

Best,

Otakar Smrz
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Existentially-quantified constructors: Hugs is fine, GHC is not?

Einar Karttunen
On 10.05 13:27, Otakar Smrz wrote:
>    data ... = ... | forall b . FMap (b -> a) (Mapper s b)
>
>    ... where FMap qf qc = stripFMap f q
>
> the GHC compiler as well as GHCi (6.4.2 and earlier) issue an error
>
>     My brain just exploded.
>     I can't handle pattern bindings for existentially-quantified
>     constructors.

You can rewrite the code in a way that GHC accepts it. Just
avoid pattern binding your variables. I had the same problem
in HAppS code and needed to lift some code to the top
level to solve it.

- Einar Karttunen
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Existentially-quantified constructors: Hugs is fine, GHC is not?

Ben Rudiak-Gould
In reply to this post by Otakar Smrz
Otakar Smrz wrote:
>    data ... = ... | forall b . FMap (b -> a) (Mapper s b)
>
>    ... where FMap qf qc = stripFMap f q
>
> the GHC compiler as well as GHCi (6.4.2 and earlier) issue an error
>
>     My brain just exploded.
>     I can't handle pattern bindings for existentially-quantified
>     constructors.

The problem here is a tricky interaction between irrefutable pattern
matching and existential tuples. In Core, the FMap constructor has a third
field which stores the type b, and when you match against the pattern (FMap
qf qc) you're really matching against (FMap b qf qc). (stripFMap f q) might
evaluate to _|_, in which case, according to the rules for irrefutable
matching, all of the pattern variables have to be bound to _|_. But type
variables (like b) can't be bound to _|_.

 From an operational standpoint, the problem is that the (fully-evaluated)
value of b has to be available in the body of the let statement, which means
that (stripFMap f q) must be evaluated before the body, and the let
statement must diverge without reaching the body if (stripFMap f q)
diverges, since no value can be assigned to b in that case. But the
semantics of let clearly require that execution always proceed to the body
no matter what (stripFMap f q) evaluates to.

So I'm not convinced that your program is well-typed, even though it looks
fine at first. I'm not sure what happens to Haskell's semantics when you
allow type variables to be bound to _|_. The fact that Hugs allows it may be
a bug.

-- Ben

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Existentially-quantified constructors: Hugs is fine, GHC is not?

Ross Paterson
On Thu, May 11, 2006 at 01:46:43PM +0100, Ben Rudiak-Gould wrote:

> Otakar Smrz wrote:
> >   data ... = ... | forall b . FMap (b -> a) (Mapper s b)
> >
> >   ... where FMap qf qc = stripFMap f q
> >
> >the GHC compiler as well as GHCi (6.4.2 and earlier) issue an error
> >
> >    My brain just exploded.
> >    I can't handle pattern bindings for existentially-quantified
> >    constructors.
>
> The problem here is a tricky interaction between irrefutable pattern
> matching and existential tuples. In Core, the FMap constructor has a third
> field which stores the type b, and when you match against the pattern (FMap
> qf qc) you're really matching against (FMap b qf qc). (stripFMap f q) might
> evaluate to _|_, in which case, according to the rules for irrefutable
> matching, all of the pattern variables have to be bound to _|_. But type
> variables (like b) can't be bound to _|_.
>
> From an operational standpoint, the problem is that the (fully-evaluated)
> value of b has to be available in the body of the let statement, which
> means that (stripFMap f q) must be evaluated before the body, and the let
> statement must diverge without reaching the body if (stripFMap f q)
> diverges, since no value can be assigned to b in that case. But the
> semantics of let clearly require that execution always proceed to the body
> no matter what (stripFMap f q) evaluates to.
>
> So I'm not convinced that your program is well-typed, even though it looks
> fine at first. I'm not sure what happens to Haskell's semantics when you
> allow type variables to be bound to _|_. The fact that Hugs allows it may
> be a bug.

Why would a type variable be present at runtime, let alone bound to _|_?

I believe the Hugs behaviour was intentional.  It's particularly
handy with single-constructor data types, e.g. representing objects.
It does complicate the formal specification of pattern matching a bit,
but I don't think it's unsound in any way.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe