Opened 6 years ago

Last modified 22 months ago

#5590 new feature request

"guarded instances": instance selection can add extra parameters to the class

Reported by: nfrisby Owned by: simonpj
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.2.1
Keywords: 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:


Disclaimer: the same semantics can currently be achieved without this syntax. So this is mostly a Parser request, though I've made it a Type Checker request because some type errors would probably need to be aware of the language extension. More on this at the bottom.

We'll start with a demonstration. Just some ancillary declarations for now.

class Sat t where dict :: t

data True; data False
type family Pred (p :: * -> *) a

type family Left  a; type instance (Either l r) = l
type family Right a; type instance (Either l r) = r

data Path p a where
  Here :: p a -> Path p a
  L :: Path p l -> Path p (Either l r)
  R :: Path p r -> Path p (Either l r)

The objective of these declarations is to allow us to define some Predicate p and use the Sat class to find a path leading through a tree of Eithers to a type that satisfies that Predicate.

These next three declarations use the new syntax, as I'm imagining it.

-- NB new syntax: `guard' keyword, the pipe after the instance head,
-- and a comma-separated list of types after that
instance guard Sat (Path a)
  | Pred p a, Pred (Path p) (Left a), Pred (Path p) (Right a)

-- now we match on the instance guards, using the same pipe syntax
instance Sat (p a)      => Sat (Path p a)            | True , satl , satr where
  dict = Here dict
instance Sat (Path p l) => Sat (Path p (Either l r)) | False, True , satr where
  dict = SL dict
instance Sat (Path p r) => Sat (Path p (Either l r)) | False, False, True where
  dict = SR dict

The guard declaration asserts that any instance of Sat with a head that would overlap a la OverlappingInstances with Path a shall be disambiguated via the comma-separated list of types following the pipe. In this example, the subsequent three instances, which would traditionally overlap, are indeed disambiguated by their additional "instance head guards" (cf. HList's type-level programming style: AdvancedOverlap).

We can currently simulate this syntax by declaring a variant class of `Sat' which takes an extra parameter and thread the instance guards through that. Unfortunately, this workaround is repetitive, misses out on the better type error messages possible with specific Type Checker support, and it's just a bother.

class Sat_ a anno where dict_ :: anno -> a

instance (anno ~ (Pred p a, Pred (Path p) (Left a), Pred (Path p) (Right a)),
          Sat_ (Found a) anno) => Sat (Path p a) where
  dict = dict_ (undefined :: anno)

instance Sat (p a) => Sat_ (Path p a) (True, satl, satr) where
  dict_ _ = Here dict

In the spirit of #4259, total type families, and AdvancedOverlap, this syntax could be enriched and thereby promoted to an actual Type Checker extension. Replacing the comma-separated list of types in the guard declaration with a sequence of contexts would be appropriate syntax for explicitly making instance selection sensitive to those contexts. The instance head guards could then just be a type boolean (wired-in to the compiler, now) indicating whether the context was satisfied. A True would bring that context's consequences to bear within both the instance's own context and its declarations. For example, we could do without the Left and Right type families.

instance guard Sat (Path a)
  | (Pred p a) (a ~ Either l r, Pred (Path p) l) (a ~ Either l r, Pred (Path p) r)

instance Sat (p a) => Sat (Path p a) | True satl satr where
  dict = Here dict

Change History (10)

comment:1 Changed 6 years ago by nfrisby

In case more motivation is needed; this example is one I find particularly compelling, Conal Elliott's TypeCompose. With just the semantically-conservative extension:

data Pos; data Neg; type family Polarity (f :: * -> *)

instance guard Functor (g :. f) | Polarity g, Polarity f

instance (  Functor g,   Functor f) => Functor (g :. f) | Pos, Pos where fmap = fmapFF
instance (Cofunctor g, Cofunctor f) => Functor (g :. f) | Neg, Neg where fmap = fmapCC

This also the AdvancedOverlap stuff. With that extra power, we can be more direct.

instance guard Functor (g :. f) | (Functor f, Functor g) (Cofunctor f, Cofunctor g)

-- NB some *->* can satisfy both Functor and Cofunctor
instance Functor (g :. f) | True co where fmap = fmapFF
instance Functor (g :. f) | False True where fmap = fmapCC

comment:2 Changed 6 years ago by nfrisby

Agda's with-patterns seems similar…

comment:3 Changed 6 years ago by igloo

Milestone: 7.6.1
Owner: set to simonpj

comment:4 Changed 6 years ago by nfrisby

Yet more motivation: guarded instances would simply the approach to "overcoming overlapping instances", as described by Oleg here. (Indeed, that's the same context in which I thought of the feature.)

In particular, "guarded instances" would mitigate the need for "replica classes", such as his ShowList'.

comment:5 Changed 6 years ago by simonpj

difficulty: Unknown

I'm afraid I do not understand the proposal in this ticket, yet anyway; an example or two doesn't tell me its syntax, static semantics, internal language, or dynamic semantics.

Can I invite to to look at NewAxioms? Maybe it covers similar territory?

comment:6 Changed 5 years ago by igloo


comment:7 Changed 3 years ago by thoughtpolice


Moving to 7.10.1.

comment:8 Changed 3 years ago by thoughtpolice


Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:9 Changed 2 years ago by thoughtpolice


Milestone renamed

comment:10 Changed 22 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.