GADTing Fundeps? - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Sandy Maguire

I would expect this to work, but it doesn't.

class Model a b | a -> b where
  model :: a -> b

data Temp b where
  Temp :: Model a b => b -> Temp a

getTemp :: Model a b => Temp a -> b
getTemp (Temp a) = a
/home/sandy/Vik.hs:11:20: error:
    • Couldn't match expected type ‘b’ with actual type ‘b1’
      ‘b1’ is a rigid type variable bound by
        a pattern with constructor:
          Temp :: forall a b. Model a b => b -> Temp a,
        in an equation for ‘getTemp’
        at /home/sandy/Vik.hs:11:10-15
      ‘b’ is a rigid type variable bound by
        the type signature for:
          getTemp :: forall a b. Model a b => Temp a -> b
        at /home/sandy/Vik.hs:10:1-35
    • In the expression: a
      In an equation for ‘getTemp’: getTemp (Temp a) = a
    • Relevant bindings include
        a :: b1 (bound at /home/sandy/Vik.hs:11:15)
        getTemp :: Temp a -> b (bound at /home/sandy/Vik.hs:11:1)
   |
11 | getTemp (Temp a) = a
   |
Sandy Maguire

shouldn't the fundep here be enough to unify b ~ b1?

Sandy Maguire

given that model is library code i want to interface with, how can i do this?

Sandy Maguire

more generally the problem i'm trying to solve is that given some opaque datatype A that i can define arbitrarily to my liking, and an instance Model A B, i want to write a bunch of code that uses B but refers to A in the type signature

Sandy Maguire

but sandy! you must be mad!

Vladimir Ciobanu

getTemp (Temp a) = a is pretty confusing, tripped me up for a minute. It's probably easier to read if you replaced the as with bs :D

Vladimir Ciobanu

But I would have also expected that to work

Sandy Maguire

i want to write code of the form:

f :: A -> whatever
f = something with (model a)

and then invoke it with something like f (unmodel $ something of type B)

Sandy Maguire

such that the definition of A and unmodel are entirely mechanical and require no thought from me whatsoever as the user of this library

Vladimir Ciobanu

Model is library code is what makes this particularly hard I think

Vladimir Ciobanu

Because trying out stuff like making it an associated type rather than fundep is out of the question (not even sure if it would fix the problem)

Sandy Maguire

i think this is a bug in ghc

Sandy Maguire

i don't think it can be a tyfam because the injectivity goes the wrong way

Sandy Maguire

nevermind; the injectivity annotation isn't necessary in the tyfam

Sandy Maguire

datatype context doesn't work due to NOT WORKING ON GADTs

Sandy Maguire

oh i wonder if i can do a dumb trick

Sandy Maguire

this doesnt work :(

class Model a b => Model2 a where
  type TheModel a
instance Model a b => Model2 a where
  type TheModel a = b
Alexis King

@Sandy Maguire That isn’t a bug in GHC, it’s the way fundeps are designed (for better or for worse). Fundeps don’t provide evidence the way type equalities against type families do, they just affect type inference.

Alexis King

What does that mean in practice? It means that if you have

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

and you end up with a C Int a given, you cannot deduce a a ~ Bool given! Instead, all the fundep does is cause a new a ~ Bool wanted to be emitted. If a is a solver variable, this makes nice things happen: a will be solved to Bool, and you get nice type inference. But if a is rigid, you get nothing: you just end up with an a ~ Bool wanted that you cannot solve.

Alexis King

You can see this for yourself by writing the following very simple program:

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

foo :: C Int a => a :~: Bool
foo = Refl

This program will not compile.

Alexis King

You have to think of fundeps as “inference guides,” not sources of evidence. (The formal term for this “inference guiding” is “improvement,” introduced by Mark P. Jones in his work on qualified types.) Unless something fundamental changes in GHC’s treatment of functional dependencies, you will never be able to acquire type equality evidence from a functional dependency alone, since it simply doesn’t exist.

Alexis King

The type family equivalent works because you explicitly pass around evidence for a type equality. If you write

class C1 a where
  type B a
instance C1 Int where
  type B Int = Bool

class b ~ B a => C2 a b | a -> b
instance (C1 a, b ~ B a) => C2 a b

then when you write foo, it typechecks because you can get the a ~ B Int evidence out of the C2 dictionary’s superclass dictionaries.

Alexis King

(It can be helpful to think of a ~ b constraints as implicitly-passed a :~: b values, since in GHC, that’s exactly what they are.)

Sandy Maguire

that's helpful, thanks @Alexis King .

Sandy Maguire

apparently i've been away from Hs too long! I didn't even think about passing around :~:s

Sandy Maguire

maybe it's just because it's early and i'm still in bed, but i don't see how to make this work with explicit Refls either

Sandy Maguire

i came up with a boring solution :)

Sandy Maguire
newtype Opaque a = Opaque { getOpaque :: a }
  deriving (Eq, Ord, Show, Enum, Bounded, Read, Semigroup, Monoid)

instance Arbitrary a => Arbitrary (Opaque a) where
  arbitrary = fmap Opaque arbitrary

instance Model (Opaque a) a where
  model = getOpaque