Type Inference behaving non intuitively with Functional Dependencies

Learn
#1

Hi! So… I’m defining a small language that’s defined as follows:

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE QuantifiedConstraints #-}

module Test where 

import Data.Kind (Type)

class RValue a b  | a -> b where
  rvalue :: a -> b

class Lift a b  | a -> b where
  inject :: a -> b

type EmbeddedValue m a = m (Value m a)
type EmbeddedLazy  m a = m (Lazy  m a) 

class Exp m where
  data Value m a :: Type
  data Lazy  m a :: Type
  data Z'    m   :: Type
  val     :: Int -> m (Value m (Z' m))
  defer  :: (Lift a (m b))
    => a -> m (Lazy m b)

class Exp m => Act m where

  data VariableData m a :: Type
  halt :: m ()
  show :: forall a b. (Show a, RValue b (m a)) => String -> b -> m ()

-- Please remember this!
class Declarable m b a | m b -> a where
  declare :: b -> m a

type Constraints m =
  ( ExpConstraints m
  , DeclarableConstraints m
  , ActConstraints m
  )


-- Type judgements, don't mind
type ExpConstraints m =
  ( Monad m
  , Exp m
  -- RValues
  , m (Lazy m (Value m (Z' m))) `RValue` EmbeddedValue m (Z' m)  
  , forall a. m (Lazy m (Lazy m a)) `RValue` EmbeddedLazy m a
  , EmbeddedValue m (Z' m) `RValue` EmbeddedValue m (Z' m)
  , Value m (Z' m) `RValue` EmbeddedValue m (Z' m)
  , Lazy m (Value m (Z' m)) `RValue` m (Value m (Z' m))
  , forall a. Lazy m (Lazy m a) `RValue` EmbeddedLazy m a
  -- Variable Data RValue Unfold
  , VariableData m (m (Lazy m (Value m (Z' m)))) `RValue` EmbeddedValue m (Z' m)  
  , forall a. VariableData m (m (Lazy m (Lazy m a))) `RValue` EmbeddedLazy m a
  , VariableData m (EmbeddedValue m (Z' m)) `RValue` EmbeddedValue m (Z' m)
  , VariableData m (Value m (Z' m)) `RValue` EmbeddedValue m (Z' m)
  , VariableData m (Lazy m (Value m (Z' m))) `RValue` m (Value m (Z' m))
  -- Lift
  , forall a. m (Value m a) `Lift` m (Value m a)
  , forall a. Value m a `Lift` m (Value m a)
  , forall a. Lazy m a `Lift` m (Lazy m a)
  , forall a. m (Lazy m a) `Lift` m (Lazy m a)
  -- Variable Data Lift Unfold
  , forall a. VariableData m (Value m a) `Lift` m (Value m a)
  , forall a. VariableData m (Lazy m a) `Lift` m (Lazy m a)
  )


type DeclarableConstraints m =
  ( Monad m 
  , forall a. Declarable m (m (Value m a)) (VariableData m (Value m a))
  , forall a. Declarable m (Value m a) (VariableData m (Value m a))
  , forall a. Declarable m (VariableData m (Value m a)) (VariableData m (Value m a))
  , forall a. Declarable m (m (Lazy m a)) (VariableData m (Lazy m a))
  , forall a. Declarable m (Lazy m a) (VariableData m (Lazy m a))
  , forall a. Declarable m (VariableData m (Lazy m a)) (VariableData m (Lazy m a))
  )

type ActConstraints m = 
  ( ExpConstraints m
  , Act m
  )

(The language is larger, but this subset will do). After defining everything, I wanted to try it outa very simple example:

example2 :: forall m. Constraints m => m ()
example2 = do
  x   <- declare u/m $ val @m 50
  pure ()

Nevertheless, this fails to compile due to some ambiguous type var:

[1 of 1] Compiling Test             ( src/Test.hs, interpreted )

src/Test.hs:93:10: error:
    * Could not deduce (Declarable m (m (Value m (Z' m))) a0)
        arising from a use of `declare'
      from the context: Constraints m
        bound by the type signature for:
                   example2 :: forall (m :: * -> *). Constraints m => m ()
        at src/Test.hs:91:1-43
      The type variable `a0' is ambiguous
      Relevant bindings include
        example2 :: m () (bound at src/Test.hs:92:1)
    * In the first argument of `($)', namely `declare @m'
      In a stmt of a 'do' block: x <- declare @m $ val @m 50
      In the expression:
        do x <- declare @m $ val @m 50
           pure ()
   |
93 |   x   <- declare @m $ val @m 50
   |          ^^^^^^^
Failed, no modules loaded.

I find it a bit unintuitive, since declare only needs to know about the monad (given explicitly by the type annotation), and it’s argument (which is known, since if I add a type hole x <- declare @m $ (val @m 50 :: _), it infers a concrete type) in order to deduce the return type, which is the ambiguous a0. Is this a bug in my GHC version (9.4.8)? Or Am I missing something on how type inference works with these extensions?

1 Like
#2

Note that if you add an instance for the matching type then it will work.

instance Declarable m (m (Value m (Z' m))) () where
  declare = undefined

I don’t understand why it doesn’t work when the constraint is packaged up as part of Constraints. Maybe GHC is unwilling to use “hypothetical” constraints to resolve functional dependencies, I’m not sure.

1 Like
#3

This does work, so I guess this is one of the occasions where functional dependencies and associated types are not interchangeable.

class Declarable m b where
  type A m b
  declare :: b -> m (A m b)

example2 :: forall m. (Declarable m (m (Value m (Z' m))), Monad m, Exp m) => m ()
example2 = do
  x   <- declare @m $ val @m 50
  pure ()
2 Likes
#4

Perhaps my glasses are fogged up, but I see no instance Declarable ... in o.p.

Haskell uses (only) declared instances to resolve FDs. Using “hypothetical” constraints would involve it in infinite chases of circular references.

1 Like
#5

Is that true? Why does this compile if so?

{-# LANGUAGE FunctionalDependencies #-}

class Foo a b | b -> a where
  fooAction :: a -> b

counterexample :: Foo [a] Int => a -> Int
counterexample = fooAction . pure

Note that it fails if the fundep is removed, because the pure is ambiguous.

1 Like
#6

It compiles because you’ve not called counterexample (nor fooAction in open code), so the compiler doesn’t (yet) need to infer any improvement. (Presumably you’re going to import this module into somewhere that provides an instance and calls the function.)

Sure. So at this stage, the compiler does at least need to check it can disambiguate the chain of inference once it sees an instance.

In your o.p., it might be GHC is smart enough these days to look at all those Declarables in type DeclarableConstraints m and discharge a Wanted (Declarable m (m (Value m (Z' m))) a0). But that Wanted is not an exact match to any. In particular (m (Value m (Z' m))) is more specific (Overlapping) than the b in any of those Declarables. So even if you don’t think you’re using OverlappableInstances or its pragmas, GHC assumes you are until it can see an instance and the module it appears in.

Yes there are lots of ‘occasions’ when you get down to gnarly possibly-overlapping constraints like this. (And Assoc Types instances can’t be overlapping – although I’m not sure if GHC takes any advantage of that. If you want overlaps you have to use a closed Type family decl, not an Assoc type.)

Also your example2's signature does give a Declarable that’s exactly the Wanted; so it’s not comparable to o.p./GHC doesn’t yet need to go looking for an instance.

1 Like
#7

If this were the actual explanation, adding type applications to declare in the example wouldn’t clear things up, would it? Because the wanted instance would still be more specific than any of the dictionaries in scope.

And yet:

example2 :: forall m. Constraints m => m ()
example2 = do
  x   <- declare @m @(m (Value m (Z' m))) @(VariableData m (Value m (Z' m))) $ val @m 50
  pure ()

works fine.

I think the actual issue here isn’t to do with overlapping constraints or the claim that GHC won’t use fundeps unless there are actual declared instances, but that quantified constraints are limited in some way.

1 Like
#8

And in fact: #15351: QuantifiedConstraints ignore FunctionalDependencies · Issues · Glasgow Haskell Compiler / GHC · GitLab

1 Like
#9

Ha ha. I see somebody with the same name as me had quite a bit to say about it. I have zero memory of that discussion.

As to the ‘meat’ of the question: what if the constraint inside the quantification improves the dependent argument in a way contradictory to any instance? Then does the compiler have to keep quantified pseudo-instances hermetically sealed apart from proper instances? Don’t we otherwise end up at unsoundness? Is that why that later example complains it can’t/won’t apply a quantified FunDep?

“Works” means you can compile the decl? Can you actually call your example2 and get it to produce a result? – which is I think the point at which o.p. fell over. I’m also interested what type gets inferred for the local x: does it include an unresolved/Wanted Declarable constraint?

I see o.p. has AllowAmbiguousTypes; are you also setting that? Then maybe all this is achieving is hiding/postponing the type errors. (For that reason I totally hate that extension. And GHC error messages often suggest switching it on, which just makes learners’ lives miserable.)

IOW I’m not convinced " adding type applications to declare in the example" is actually clearing things up as opposed to delaying where the trouble appears.

1 Like
#10

This is a nice workaround! For the time being, this should solve my issues (since every functional dependency I have has the same form: C m a b | m a -> b). But it’s a bit sad that we have to lose the the power of functional dependencies (haven’t played around with fundeps, but I’m assuming we can have things like C a b c d | a b -> c d, a c d -> b).

#11

Yes you can. And those are ‘full’ FunDeps (mention all the class params), so they are reasonably well-behaved. Beware partial FunDeps or mixing a full with a partial on the same class. Also beware overlapping instances: there’s a way to declare your instances which is robust; but other ways that will seemingly be accepted but cause trouble at usage sites.

1 Like
#12

The original code (example2) infers x to be an ambiguous type variable w0.

That’s exactly what I was trying to achieve! I was having issues to typecheck my definitions/instances, So I thought that maybe delaying the issue would eventually make it resurface in a place that I can handle it better.

If I provide the full types (i.e: declare @m @(m (Lazy m (Value m (Z' m)))) @(VariableData m (Lazy m (Value m (Z' m))))) example2 compiles and can be run with a type that properly instantiates the constraints, but I was really wishing to have better type inference.

#13

Well yes. If you’re type-@pplying the answer, what good is the FunDep doing you? There’s a bunch of wild ideas – including Wiggly arrows – whereby the FunDep arrow is more or less a lie to placate the typechecker: “don’t worry your pretty head, let’s pretend that type is determined”. And you give the actual type at usage sites. The ideas are in the same bucket as AllowAmbiguousTypes: defer reporting ambiguous types in the hope it’ll get sorted out later.

Linked from that discussion is a way of getting around the fundept [that] is terrifying [official SPJ assessment]. It’s been a stable hack for more years than anybody can guess at, and I predict it’ll remain unfixed for decades more. So you could try that (and might be able to dispense with the quantified constraints).

1 Like
#14

  • Why does Haskell have functional dependencies?

    Because multi-parameter type classes can sometimes have ambiguous instances.

  • Why does Haskell have multi-parameter type classes?

    Because the original (single parameter) type classes limited expressivity.

  • Why does Haskell have type classes?

    To provide a means of reusing symbols with different types - overloading.

Having recently seen this:

and having already seen this some time ago:

…is the very concept of a type class a mistake (or at least flawed)? Because it seems to me that the “Jenga-tower” of a type system Haskell now has is largely the consequence of that original decision.

#15

Weeell hmm. If we go back to the Mark P Jones 2000 paper that introduced FunDeps …

Because some methods within a type class don’t mention all the type params: the Collection example where insert takes args element and a collection, but empty only the collection.

For example you can’t express there’s both together a collection type and a element type.

We should also mention relaxing the H98 restriction that instance args must be of the form T a b c ... where T is a type constructor and a b c ... are bare type variables. So we can express instance Collection [a] a. But now this opens the door to overlapping instances.

The original Wadler paper txt email 1988 that introduced type classes first considered an approach of overloading the methods only, with no such thing as a type class. Pretty much like Funky [**] and the Perry thesis[***], it seems. (Wadler’s was more of a straw man to knock down and argue for type classes.) And yet the motivating argument was the Num class to define (+), (-), (*), (\), fromInt .... With a great deal of hindsight, that turned out to limit expressiveness, because you might want fromInt without any other arithmetic at all; or additive without multiplicative; or etc.

Now that we have type families (and Dependent types on the ever-receding horizon) perhaps merely overloading methods could have been a better approach?

I think we’re all being let down by GHC’s terrible implementation of FunDeps. High Command seems to have just abandoned FunDeps when the new shiny thing Type families came along. And yet TFs are unsound [****]; furthermore I hear they’re going to be phased out one day in preference for some Dep. typing mechanism. “offers to design an even more powerful [type mechanism]”.

[**] Funky just banishes ‘Colliding types’ – that is, overlapping instances. Nearly all the ‘interesting’/expressive type classes I declare rely on overlapping instances. So Funky might be good for learners, it’s no good for industrial use. And overlapping instances combined with FunDeps is one of the places where GHC is just crap.

[***] Perry seems to resort to hand-waving away overlapping (“Best fit” Overloading Resolution). I don’t see the suggestions being entertained mid-page 64 are going to scale, especially when calls to methods are deeply-nested inside calls to overloadable methods inside … [BTW your link didn’t work for me/I had to Google scholar for it.]

I think what Funky/Perry would need is some equivalent to a superclass constraint: this instance of method f T a is valid providing there’s an instance f a. But now your overloading decls are more complex than merely giving a series of equations. (And remembering that an instance for f might call an instance for g that calls … that circles back to f for a.)

Also Haskell (or at least GHC) supports separate compilation. What if the instances (or indeed whole method decls) we want are out of sight in a different module?

[****] Or ot least TFs used to be unsound in combination with GND. I don’t know whether the Coercible stuff will rescue the fort.

1 Like
#16

Your support of functional dependencies and criticism of dependent types is…“curious” - as I recall it, functional dependencies were largely responsible for poor-man’s Prolog type-level programming to gain popularity in Haskell. From that point onwards, it was only a matter of time before someone reckoned that type-level programs ought to be able to interact with the Haskell expressions being programmed typed: “next stop, dependent types!”…

It’s been a while since I last read it…but I don’t recall Perry’s overloading mechanism being quite so “exclusionary”. But if I’m also wrong there - system CT would be closer to Haskell’s style of overloading (if restricted to the top level); maybe it could be extended just enough to allow for some form of overlapping.

I believe the system CT research mentioned something about that too…

Hooray - it isn’t just “my end of cyberspace” that’s having this problem with the older CiteSeerX links! (I know of at least one local library whose computers also display that darned Token is required nonsense, but I wanted someone elsewhere in cyberspace to report back with the same problem, just to be absolutely sure - thanks!)

1 Like
#17

So, I tried changing the Functional Dependency and the constraint to:

class Declarable m b where
  type DA m b :: Type 
  declare :: b -> DA m b

(...)

type DeclarableConstraints m =
    ( Monad m 
    , Declarable m (m (Value m (Z' m))) 
    , forall a. DA m (m (Value m a)) ~ m (VariableData m (Value m a))

Nevertheless, this fails with:

[1 of 1] Compiling Test2            ( src/Test2.hs, interpreted )

src/Test2.hs:80:1: error:
    * Illegal type synonym family application `DA
                                                 m (m (Value m a))' in instance:
        DA m (m (Value m a)) ~ m (VariableData m (Value m a))
    * In the quantified constraint `forall a.
                                    DA m (m (Value m a)) ~ m (VariableData m (Value m a))'
      In the type synonym declaration for `DeclarableConstraints'
   |
80 | type DeclarableConstraints m =
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Failed, no modules loaded.

Which is understandable, but sadly the same issue.

I don’t think I can relax the Quantified Constraint (I cannot delete it since that’s what gives me “type checking” in my eDSL, nor “expand” the forall since I have infinite types, i.e: Lazy (Lazy (Lazy ....)). So for the time being I think I hit a big wall.

#18

Why not replace the quantification with a separate class with an instance for each quantified constraint in DeclarableConstraints?

#19

Not true! Here’s another example. (Chiefly to explain this to myself.)

The straightforward attempt to pack an existential in one type class environment and unpack it in another module (where a more specialized instance is introduced) does not work because the existential is packed with the corresponding dictionary. When it is unpacked, the packed dictionary is used – regardless how many new instances become available.

That was from 9 years ago, but I doubt GHC has changed since.

So inside quantified constraints, FunDeps are ignored (irrespective of instances in the environment). Inside existentials/GADTs, instances are ignored. Then there’s plenty ways to see inconsistent type improvement. That issue thinks it unlikely you’ll get unsoundness.

1 Like