Opened 3 years ago

Last modified 2 years ago

#12647 new task

Can't capture improvement of functional dependencies

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: None Version: 8.0.1
Keywords: FunDeps Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Type Families with Class, Type Classes with Family discusses instance improvement with the example

class Collection c e | c -> e where
  empty :: c
  add   :: e -> c -> c

instance Collection [a] a where
  empty :: [a]
  empty = []

  add :: a -> [a] -> [a]
  add = (:)

I wondered how to express that x ~ Int can be deduced from Collection [Int] x using improvement, I first attempted using the constraints machinery:

data Dict c where
  Dict :: c => Dict c

newtype a :- b = Sub (a => Dict b)

but I'm not able to construct a term of type Collection [Int] x :- (Int ~ x) proving that Collection [Int] x entails Int ~ x:

ghci> Sub Dict :: Collection [Int] x :- (Int ~ x)

<interactive>:52:5: error:
    • Couldn't match type ‘x1’ with ‘Int’ arising from a use of ‘Dict’
      ‘x1’ is a rigid type variable bound by
        an expression type signature:
          forall x1. Collection [Int] x1 :- Int ~ x1
        at <interactive>:52:13
    • In the first argument of ‘Sub’, namely ‘Dict’
      In the expression: Sub Dict :: Collection [Int] x :- (Int ~ x)
      In an equation for ‘it’:
          it = Sub Dict :: Collection [Int] x :- (Int ~ x)

Is this due to overlapping instances or something?

Change History (5)

comment:1 Changed 3 years ago by goldfire

Functional dependencies, as implemented in GHC, are used purely for disambiguating otherwise-ambiguous variables. That's it! In particular, a "given" fundep goes unused.

There is much room for improvement here, but it would take a dedicated soul, and quite likely an update to the core language, with proofs and possibly a paper.

comment:2 Changed 3 years ago by Iceland_jack

Thanks for the response!

Interesting, since I'm maintaining notes on type classes what should I say about ​instance improvement, that it's not supported by the compiler or is it more complicated?

comment:3 Changed 3 years ago by goldfire

Instance improvement happens only when you have a "wanted" constraint -- that is, when you're typechecking a function call of f where f has a class constraint with a functional dependency.

Does that help?

comment:4 Changed 3 years ago by rwbarton

See related discussion at http://stackoverflow.com/questions/34645745/can-i-magic-up-type-equality-from-a-functional-dependency/, #11534, and various other Trac tickets linked from there.

comment:5 Changed 2 years ago by simonpj

Keywords: FunDeps added; FunctionalDependencies removed
Note: See TracTickets for help on using tickets.