System FC for FunDeps: not doing what it says on the tin

added FunctionalDependencies Tbug labels

The paper is perhaps misleading. GHC does not translate fundeps to FC; it just uses them to guide unification. You have to translate yourself. Here is one version:

class (b ~ F a) => C a b where
  type F a

instance C Int Bool where
  type F Int = Bool

class D a where { op :: C a b => a -> b }
instance D Int where { op _ = True }

Schrijvers et al have a paper describing a systematic translaiotn

The paper Simon mentions is here.

You have to translate yourself. Here is one version:
   class (b ~ F a) => C a b where
     type F a

Oh. >scales fall from eyes<

Schrijvers et al have a paper describing a systematic translaiotn

I'd up til now taken it that the translation produces equivalent code. This is the first time I've heard someone say out loud that Type Family + ~ constraint produces stronger type improvement than a FunDep.

That perhaps explains some previously mystifying (to me) comments on proposals about type-level evidence for ~ constraints.

Then is there any (good) reason why the original class F a b | a -> b doesn't/couldn't actually be equivalent? What 'goes wrong'?

(It's probably true that FunDeps never have done that: Hugs similarly rejects the original code.)

That's right: fundeps have never done that, since day 1.

Here's one way to express it: into what statically-typed intermediate language might we compile fundeps?

One possible answer (A) is: System FC. That would mean implementing a transformation like the one above -- details in Schrijers.

Another possible answer (B) would be (somehow) to support fundeps directly in the intermediate language. But you want that intermediate language to be robust to all sorts of program transformations, to enjoy progress and type-preservation etc... It's entirely possible that such a language exists, but no one has proposed one.

At the moment the fundep -> type-family translation is not implemented in GHC; you have to do it manually. It could probably be automated, but that would have a significant cost in terms of compiler complexity that would have to be weighed against the benefit.

Thank you Simon,

I'm taking it that the absence of a negative answer to my "What goes wrong?"; and the discussion of possible approaches is saying 'nothing would go wrong'(?)

into what statically-typed intermediate language might we compile fundeps?

There's only one answer to that for GHC: System FC. I'm continuing to monitor the evolution of implication constraints, because that strikes me as the mechanism for translation.

class F a b | a -> b
instance F Int Bool

generates a Given

(forall b. F Int b => b ~ Bool)

Note this requires proving F Int b before firing the improvement for b, so its semantics are different to the nasty unconstrainedness of Type Families.

Then how do implication constraints get compiled into FC?

Then is there any (good) reason why the original class F a b | a -> b doesn't/couldn't actually be equivalent? What 'goes wrong'?

Indeed, nothing goes wrong. You just have to implement the Schrijvers-et-al translation. Which you could do manually (by changing the source code) or automatically (by getting GHC to transform the source code).

monitor the evolution of implication constraints, because that strikes me as the mechanism for translation.

Yes, it half-works at 8.6.1, perhaps 8.6.4 fixes the apparent looping? Here's a couple of instances for demo

{-# LANGUAGE  QuantifiedConstraints #-}

class (forall b. F Int    b => b ~ Bool,
       forall b. F String b => b ~ Char)
      => F a b  | a -> b
instance F Int    Bool
instance F String Char

class D a where { op :: F a b => a -> b }
instance D Int    where { op _ = True }
instance D String where { op _ = 'c' }

This compiles and infers op "hello" :: Char. But running it seems to go into an infinite loop (is that a bug?). All of these ingredients are needed (without them it doesn't compile, or fails to infer type improvement):

Implication constraints superclass F, not on the instance.
FunDep.
Instances duplicating the Implic constraints. (That is, a dummy instance F a b won't get there.)
But note I don't need to change the 'client' class D.

@ulysses4ever The paper [Schrijvers et al] Simon mentions is here.

Thanks Artem, I know it well. It focuses on Trac #9627, which is very similar to this ticket.

I'm a lot less than convinced, see my comments following Tom volunteering it here.

IMO there's two reasons people continue to use FunDeps despite Assoc Types/Type Families being available for nearly a decade:

TF code is more verbose: it's not the TF instances alone (that duplicate class instances), but also all the ~ constraints you end up adding to other instances that mention the TF. Then even if Schrijvers et al can auto-gen/hide the TF code representing the FunDep, I suspect the contagion will still spread elsewhere. There's heaps of packages on Hackage that have been recoded to use TFs, but people continue to prefer the FunDep versions.
Overlapping Instances: nobody in GHC HQ is working on the theory for them -- and this goes back to the CHRs paper in 2006. Schrijvers et al continue to ignore them; then I don't think the proposal 'pays its way'.

If I'm such a bigmouth, how would I handle Overlaps? I suspect, again, there's a way with implication constraints, but it needs more compiler support than we have today. This is indicative (but doesn't work)

instance                        F (Maybe Int) Int
instance {-# OVERLAPPABLE #-} 
         (a' /~ Int, b ~ ()) => F (Maybe a' ) b
                    -- i.e.     F (Maybe a' ) ()

class (        -- implics for other instances, as above
       forall b. F (Maybe Int) b => b ~ Int,  -- regular implic
       forall a' b. (F (Maybe a') b, a' /~ Int) => b ~ ())
      => F a b  | a -> b

The /~ can be defined today as an ordinary type operator:

type (/~) a b = (a == b) ~ False

                -- (==) is a TF defined in Data.Type.Equality

But putting /~ in a constraint on lhs of => implication, GHC just barfs that it can't see what's going on.

mentioned in issue #16442

I'm not ever-so convinced this is a FunDeps issue or even a typeclass constraint issue. I notice with both this example and #9627, the class with the FunDep has no methods. (Is a methodless FunDep the counterpart of an unconstrained/non-associated Type Family and the difficulties with that?) Consider this variant, which expresses the FunDep in an explicit method:

class F2 a b | a -> b  where { dummyMeth :: a -> (b -> b) }
instance F2 Int Bool   where { dummyMeth    _ =  id }

class D a where { op :: a -> b }        -- removed the constraint
instance D Int where { op x = dummyMeth x True }

This is also rejected, same message

* Couldn't match expected type `b' with actual type `Bool'
  `b' is a rigid type variable bound by
    the type signature for:
      op :: forall b. Int -> b

Let me rephrase that 'what goes wrong?' question (this also applies mutatis mutandis for #9627):

In the type signature for method op, a is constrained by the method's class, but b is not, so it gets forall'd.
So b is a rigid type variable, and the method overload for op must cater for b being substituted at any type at all. This feels like impredicativity (sorry I can't find a more scientific term than "feels like"). The original method signature for op could equivalently be
```
  class D a where { op :: a -> (F a b => b) }
```
This needs RankNTypes to compile, but GHC then infers op :: (D a, F a b) => a -> b, which is back where we started.
OK so what goes wrong if a method overloading yields a less general type for the rigid type variable?
In the case of #9627, just avoid giving a signature for the function; applying dummyMeth will raise a Wanted C Int b and immediately discharge it on instance C Int Bool.
With this example, the signature can't be avoided: it comes from the signature given for op in the class decl.
If the usage site for op wants anything other than Bool, such as op (5 :: Int) == 'c', that'll get rejected as usual. (The rejection might be: no instance for F Int Char.)

I'm getting a bit lost. The question (for me) is: what is the statically typed intermediate language; and what is the translation from Haskell into that intermediate language. Does your comment bear on this question? Or are you addressing something else? Sorry to be dim.

You're not being dim. We are talking at cross-purposes.

To ask about how an implementation translates into some other semantic representation (an intermediate language) is to assume we already know what the semantics is or should be.

The questions for me (and I think with the Original Post for #9627; and with the 2011 System FC paper) is: is there anything unclear about the semantics? is there something goes wrong such that rigid type variables cannot be instantiated by something less general than a bare var? why are these programs with FunDeps rejected?

The desired typing seems clear. (It's exactly the typing that GHC and Hugs infers if you put instance D Int where { op _ = undefined } and ask for :t op (5 :: Int), yielding :: Bool.) Then the given overloading/equation for method op _ = True type-checks. But it might be that these examples are too simplistic; that trying for a general specification ends up at undecidability or non-termination?

If 'nothing goes wrong', then why don't Hugs/GHC already accept such programs and implement that clearly-defined typing and semantics? Why didn't they do that (say) back in 2006 when the 'via CHRs' paper specified the semantics, before there were Type Families or System FC?

Note these examples don't involve any of the gnarly bits of FunDeps such as overlaps or UndecidableInstances. But a general specification would have to consider those, which is why neither the 2006 CHRs paper nor the Schrijvers et al translation are adequate IMO.

Or are you saying that System FC is the only way to specify the semantics for Haskell/or for Haskell extensions beyond the 2010 Report? And that (for the general case) overlapping instances with FunDeps must translate to Closed TFs?

Or are you saying that System FC is the only way to specify the semantics for Haskell/or for Haskell extensions beyond the 2010 Report?

Pretty much yes. Not because it's perfect but because I don't know anything better.

The standard way to specify the semantics of a language is

A static semantics, usually expressed as a collection of typing rules, that say which programs are well-typed and which programs are not.
A dynamic semantics, that specifies what happens when the program is executed. This can be a denotational semantics or an operational one.

In a language as complex as Haskell, giving a precise formal account of the above is quite a challenge. So the way that we have evolved for Haskell is to give a formal static and dynamic semantics for a small "core language" (that's System FC), and a translation from Haskell into that core language.

I don't know anyone who has given a formal static and dynamic semantics for a language with functional dependencies. That would be a worth goal, if you or anyone else wanted to undertake it.

I don't know anyone who has given a formal static and dynamic semantics for a language with functional dependencies.

I think you're being a drama queen/scare-mongering. GHC HQ just wants to wash its hands of FunDeps. We don't need to give end-to-end semantics for FunDeps. It's sufficient to translate a program with FunDeps into a Haskell without FunDeps (but still with MultiParamTCs); then proceed through "the way that we have evolved".

And we have plenty of prior art for how to translate-away the FunDeps: both Mark P Jones' original work; and the 'via CHRs' paper that expanded on it, including all the relaxed/liberal coverage conditions stuff whose good disciplines GHC continues to ride roughshod over.

If you're saying you don't know how to improve GHC, because the only tool to hand is System FC, that sounds to me like FC is not fit for this purpose. The 'via CHRs' work uses the tools of First Order Logic (specifically FOL with equality to give type unification). It's the 'implicational fragment' of FOL, chosen deliberately so that FunDeps derivations are decidable and terminating.

Then that's why I've tried above to couch the improvement in terms of surface-language quantified/implication constraints:

a) because that fits with First Order Logic;

b) because I stand a hope of expressing overlap logic using FOL.

However which way I try to hand-translate FunDep code into non-FunDep Haskell, I bump into inadequacies in GHC/presumably inadequacies in FC:

The quantified implication constraints cause looping #16442.
GHC can't see the logic needed for type disequality constraints/implications. (What it needs there is to expose the logic already in play with Closed Type Family instance resolution.)
If I avoid implication constraints, I get these dratted rigid type variable rejections that are preventing code for which (you keep telling me) 'nothing goes wrong'.

To rework the running example how I want

class F a b | a -> b
instance F Int Bool

class D a where { op :: F a b => a -> b }
instance D Int where { op _ = True }

the class decls stand as is; the instances become

instance (b ~ Bool) => F Int b        -- the constraint represents an implication

instance D Int where { op _ = True :: F Int b => b }
                             -- match the `F` instance
                             -- translate from its implication
instance D Int where { op _ = True :: b ~ Bool => b }

Rejected: b is a rigid type variable.

What 'goes wrong' if b's type is less general than a bare tyvar? You're telling me: nothing.

An alternative approach to translating from FunDeps is to stretch an existing GHC extension a bit further ...

Currently InstanceSignatures allow giving a more general type to class parameters than would be expected from the instance header. We could make it work harder by allowing it for non-parameter types to give a more specific type:

instance D Int where {
    op :: (F Int b, b ~ Bool) => Int -> b
    op _ = True
    }

That signature could be more succinctly op :: Int -> Bool. I'm not suggesting the code needs to be written like that [*]. Rather, that translating-away FunDeps generates those InstanceSignatures.

[*] Because if you had to write it like that, it would be not much more code to make D a two-parameter class with a FunDep. Therefore with instances that duplicate F's. And for #9627 turn the function into a method.

I apologise. I was just trying to address your question

Or are you saying that System FC is the only way to specify the semantics for Haskell/or for Haskell extensions beyond the 2010 Report?

To which my answer is "no, that's not the only way; here is an alternative".

Perhaps you are saying "let's specify fundeps by

a) specifying a translation from Haskell-with-fundeps into Haskell-with-type families, and

b) specifying or implementing Haskell-with-type-families"?

Yes, that is a fine path. I think it's the one that Schrijvers et al have followed. However I think you are perhaps suggesting an alternative translation for (a).

Yes #16442 looks like a bug to me. I have started to investigate.

As to rigid type variables, this program is indeed rejected

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}

module Foo where

class F a b

class D a where { op :: F a b => a -> b }

instance (b ~ Bool) => F Int b

instance D Int where { op _ = True }

And indeed it should be. In the instance declaration for D Int we are asking that True :: forall b. F Int b => b, and that simply doesn't hold. From the given constraint F Int b we can deduce the superclasses of `F, but we cannot deduce the preconditions of the instance. For example, suppose whave

instance Show a => Ord [Tree a] where ...

Then in a function definition

f :: Ord [Tree a] => blah

we cannot make use of Show a. (We can make use of Eq [Tree a].)

However the translation of Schrijvers et al works out fine. This compiles

class (b ~ Fb a) => F a b where
  type Fb a :: *

instance (b ~ Bool) => F Int b where
  type Fb Int = Bool

class D a where { op :: F a b => a -> b }

instance D Int where { op _ = True } -- :: F Int b => b }

So perhaps one way forward might be to use their translation?

perhaps one way forward might be to use their [Schrijvers et al] translation?

Not unless and until it has an approach for Overlapping Instances.

In the putative translation to non-FunDep/non-TF Haskell you give (and thank you for all the time you're putting into this), I think you've missed a step/thrown away information too early:

we're 'allowed' to take advantage of the knowledge that class F has a FunDep; therefore we are expecting a constraint that improves the dependent type param.

we cannot deduce the preconditions of the instance

Yes we can. (Perhaps what you mean is that GHC doesn't currently.) The 'via CHRs' paper Fig 2 says instance (b ~ Bool) => F Int b gives us a rule F Int b <==> (b ~ Bool) -- i.e. bi-implication. (That applies for all constraints on instances. [Note **]) I plain do not know how much (if any) of the 'via CHRs' thinking made it into GHC. Certainly not all, and that seems a real shame.

we cannot deduce what the precondition says 'in advance' of instance resolution; but we do know there is a precondition; we do know it targets the dependent type param; we do know it's a ~ constraint.

So I'm saying the translation to non-FunDep Haskell goes

True :: forall b. F Int b => b                -- and then to

True :: forall b. b ~ Bool => b

This is still rejected rigid type variable. But why? (Is what I'm asking. And not just me: there's a gazillion questions on StackOverflow.)

If we see instance D Int where { op _ = True } but we do not have in scope an instance F Int blah, then we raise Wanted ( F Int b0, b0 ~ Bool ).

in a function definition
   instance Show a => Ord [Tree a] where ...

   f :: Ord [Tree a] => blah
we cannot make use of Show a.

But if I go

f :: (Ord [Tree a], Show a) => blah

then I can make use of Show a. 'via CHRs' Fig 2 says those two signatures for f are equivalent (presuming the Ord instance is in scope; also presuming there's no risk of an Overlapping Instance).

Is the difficulty GHC's delayed/lazy instance resolution? (Which GHC does to bend over backwards for Overlapping Instances and fingers-crossed confluent type improvement; also for separate compilation where the Wanted instance is in some downstream module. That is such a darned nuisance for diagnosing instance/constraint resolution trouble that it's a major reason to prefer Hugs.)

Indeed if I give an equation for f but no signature; and the equation uses a show for an a and a comparison for a [Tree a], GHC will infer the wanted constraints just fine.

[Note **] I'd better add we can only make that move because in this example there's a single FunDep. With multiple FunDeps on a class, where a param might be a source in one but a target in another; it gets rather more complex. So the 'via CHRs' Fig 2 has a finer-grained translation. Also there weren't ~ constraints in surface Haskell at the time.

Heh, heh. I've been going round and round the houses beating my head against this. The old-fashioned typecast trick works -- but only in Hugs:

class F a b | a -> b
instance F Int Bool

class D a where { op :: (F a b) => a -> b } 
instance (TypeCast Bool b') => D Int where { op _ = typeCast True }

The TypeCast constraint is needed, as well as the typeCast method. The TypeCast constraint on the instance must be that way round (not TypeCast b' Bool, even though TypeCast has both-directions FunDep.) The TypeCast constraint looks weird with that b' dangling in mid-air.

OTOH I haven't saved much code: in effect I need to repeat the F instances as D instances, with F's second type param appearing in D's constraint. And for my real-life example (which has recursive constraints on the instances for F) I need to repeat a load of those constraints.

For #9627 typecast works rather nicely in both Hugs and GHC:

class C a b | a -> b
instance C Int Bool

f :: (C Int b, TypeCast b Bool) => b -> Bool
f x  = typeCast x

Addit: Actually #9627 works in GHC 8.6.4 absolutely fine. (Perhaps it didn't 4 years ago when first logged.)

f :: (C Int b, b ~ Bool) => b -> Bool
f x  = x

Yes per above, it needs in effect duplicating both params from the C instance into f's constraints.

TypeCast can be defined for GHC

class TypeCast a a'  | a -> a', a' -> a  where
      typeCast :: a -> a' 
instance a ~ a' => TypeCast a a'  where
      typeCast = id

Or the old-fashioned way per HList, in both GHC and Hugs.

What I still don't get is how TypeCast is not quite equivalent to a ~ constraint:

You must always put a typeCast method call, even though it resolves to id. Whereas for ~, GHC figures out in effect where to put the type equality no-op.
~ is a little more eager to unify, so GHC sees what's going on and complains about trying to unify a rigid type variable.

mentioned in issue #9627

System FC for FunDeps: not doing what it says on the tin

Child items ...

Activity