Why/how does this class/method work? (`~` constraint)

Learn
#1

Continuing the discussion from (… cont) Data.Set no Functor/Monad instance:

I threw down this code without much thought just to get something working. (I was quite surprised it worked, and even more surprised the OVERLAPPABLE instance works smoothly.)

    class Functorb (fb :: Type)  where
        fmapb :: fb ~ (f b) => (a -> b) -> f a -> f b 
    
    instance Ord b => Functorb (Set b)  where           -- with Ord b accepted
        fmapb = mapSet

    instance {-# OVERLAPPABLE #-} Functor f =>  Functorb (f b)  where           -- with Functor f accepted
        fmapb = fmap
  • in the class decl, the parameter fb doesn’t appear in the matrix of the method, but only in a constraint. Then
  • given some usage site of method fmapb, how does instance resolution ‘know’ which instance to select?
  • The class works just as well it seems (and that’s less of a surprise) with
        fmapb :: fb ~ (f b) => (a -> b) -> f a -> fb   -- result type is class param
  • Is ~ so magic that the method sig I first wrote is interpreted as the second?
#2

At a use site, we have fmapb :: (Functorb fb, fb ~ f b) => (a -> b) -> f a -> f b, which is roughly equivalent to (Functorb (f b)) => (a -> b) -> f a -> f b. So if the context determines f and b, then the appropriate instance can be selected.

More precisely, the magic that occurs with the first version is that GHC will introduce unification variables for f, a, b and fb, plus “wanted” constraints Functor fb and fb ~ f b. Solving the constraint fb ~ f b is trivial just by defining fb := f b, so fb gets substituted out.

The signature itself is not directly re-interpreted due to the presence of the equality constraint. But at use sites, the equality constraint will always be solved by the constraint solver, so they end up being equivalent in practice.

2 Likes
#3

Thanks Adam. So equality constraints are solved more eagerly than common-or-garden constraints? (I’m thinking of the Functor f or Ord b that arises from the rhs of the instances’ equations.)

In particular, instead of ~, I’ve tried using FunDep-driven TypeCast constraints. All I get is rigid type variable complaints, because (presumably) GHC won’t do the fb := f b step for ordinary constraints.

#4

GHC tries to find “most general solutions” to constraints, i.e. solutions that cannot be invalidated by information that may come along later. So if it sees wanted constraints Functorb fb and fb ~ f b then the former has no most general solution (because it is not clear which instance to pick), but the latter can always be solved by taking fb := f b (because any solution to the constraints must necessarily include that unification).

Thus the order in which constraints are solved is dynamic, because solving one constraint may make another previously-stuck constraint amenable to solution. In general equality constraints tend to get solved first, because their solutions are usually simple unifications, but this isn’t always true (e.g. if you have an equality constraint between two type families, unification may get stuck).

(Actually for compile-time performance reasons GHC tries to solve simple equality constraints by unification as early as possible, rather than strictly separating the steps to “generate a set of constraints” followed by “solve the constraints”. But the conceptual model is that it the type-checker generates a big set of constraints by walking the syntax tree, then the constraint-solver tries to solve them.)

What does your TypeCast class look like?

1 Like
#5

Oh, standard-issue per HList 2004 Appendix D:

module TypeCast  where

    class TypeCast a a'  | a -> a', a' -> a  where
      typeCast :: a -> a'
    instance (TypeCast' () a a') => TypeCast a a'  where
      typeCast = typeCast' ()
    class TypeCast' u a a'  | u a -> a', u a' -> a  where
      typeCast' :: u -> a -> a'
    instance (TypeCast'' u a a') => TypeCast' u a a'  where
      typeCast' = typeCast''
    class TypeCast'' u a a'  | u a -> a', u a' -> a  where
      typeCast'' :: u -> a -> a'
    instance TypeCast'' () a a  where
      typeCast'' _ x = x

Yeah. TypeCast goes through those extra two class indirections deliberately to avoid unifying too early: the equation fmapb = mapSet would give too specific :: (a -> b) -> Set a -> Set b whereas substituting the instance header’s (Set b) for the class’s fb wants (Functorb (Set b), TypeCast (f b1) (Set b)) => (a -> b1) -> f a -> f b1

    * Couldn't match type `f' with `Set'
      `f' is a rigid type variable bound by
        the type signature for:
          fmapb :: forall (f :: * -> *) b1 a.
                   TypeCast (f b1) (Set b) =>
                   (a -> b1) -> f a -> f b1

(Usually I can hack my way through rigid tv complaints, but I think the fb being ungrounded in the method sig’s matrix makes it all too ethereal. Switching round the order of args to TypeCast doesn’t help; sprinking a few calls to the typeCast method doesn’t either.)

Thank you for your explanations. I’m an antediluvian hacker, I know. I have a reason for wanting to translate this to Hugs, which I’ll put here if I can get it to work.

#6

mmm? not so fast. We’re at a specific usage site having allocated skolems so we want some fb0 ~ f0 b0. It’s not legit to take fb0 := f0 b0 if fb0 already has some assignment/unless that is of the form f1 b1 both skolems not ground types. Neither can we switcheroo f0 b0 := fb0 unless fb0 is of the form f1 b1 and contrariwise f0 b0 are both skolems.

Or … “because any solution … must necessarily include …” if we make that assignment without checking, then later arrive at a contradiction (ground type mis-match), we’re only exposing a contradiction that was lurking all along. Then the only bit that might have suffered is that the error reporting is maybe remote from the source of confusion(?)

#7

Ok I’ve got working what I wanted to demonstrate. I’ve reverted to a Keep It Simple, Stupid version of the constructor classes, using MultiParams but not FunDeps:

    class Functorb f b  where                     -- f :: Type -> Type
        fmapb :: (a -> b) -> f a -> f b 
    
    instance {-# OVERLAPPABLE #-} Functor f =>  Functorb f b  where        
        fmapb = fmap
    
    instance Ord b => Functorb Set b  where           -- with Ord b accepted
        fmapb = mapSet

The objective was instances for a datatype with constraints

    newtype Ord b => OrdSet b = MkOrdSet {unOrdSet :: (Set b)}     -- cheating; for demo only
                    deriving (Show)
    
    mapOrdSet :: (Ord b)  => (a -> b) -> OrdSet a -> OrdSet b      -- per H98 needs Ord a from LHS appearance of MkOrdSet
    mapOrdSet f (MkOrdSet s) = MkOrdSet $ mapSet f s       

    instance Ord b => Functorb OrdSet b  where             -- with Ord b only
        fmapb = mapOrdSet

How did I avoid the Ord a constraint on the incoming OrdSet a? I ‘reverted’ Hugs to pre-99 GHC.

application of MkT as introducing a constraint – hence the type of MkT –
but pattern-matching on MkT as eliminating a constraint.
But since the dictionary isn’t stored in the constructor [there’s nothing to eliminate, no-op]

#8

They’d be skolems inside a definition of fmapb, but at the use site they’re unknowns, not skolems. (Maybe f and b have been unified with skolems, but fb at least, not appearing in any unifiable part of the signature, must be an unknown.)