#5590: "guarded instances": instance selection can add extra parameters to the
class
---------------------------------+------------------------------------------
Reporter: nfrisby | Owner:
Type: feature request | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 7.2.1 | Keywords:
Testcase: | Blockedby:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
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
`Pred`icate `p` and use the `Sat` class to find a path leading through a
tree of `Either`s to a type that satisfies that `Pred`icate.
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:
[http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap 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, [TypeFunctions/TotalFamilies total type families],
and [http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap
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
…
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5590>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
