Existentially-quantified constructors: Hugs is fine, GHC is not?
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
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
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
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.
participants (4)
-
Ben Rudiak-Gould -
Einar Karttunen -
Otakar Smrz -
Ross Paterson