Bundling constraints with fundeps
I've got a function foo with a litany of constraints. Of course these constraints must appear in the signatures of functions that use foo , so what I'm trying to do is wrap the foo constraints in a type synonym FooCtx ab ... :: Constraint . As an example,
foo :: (A a, B b, C c, ...) => a -> b -> c
bar :: (A a, B b, C c, ...) ...
bar = ... foo ...
would become
type FooCtx a b c ... = (A a, B b, C c, ...)
foo :: (FooCtx a b c) => a -> b -> c
bar :: (FooCtx a b c) => ...
This works great if all of the types are exposed. However, I'm using functional dependencies to generate some of the types in the constraint list, and those types don't appear in the signature of foo . For example:
class Bar a b | a -> b
foo (Bar a b, ...) => a -> a
GHC won't accept type FooCtx a = (Bar ab) because b isn't bound on the LHS. Neither can I use type FooCtx ab = (Bar ab) because b isn't in scope in the signature of foo . The signature of foo would be foo :: (FooCtx a ?) => a -> a .
One unsatisfactory solution is to put one of the constraints in the foo signature with FooCtx to bring the fundep type in to scope:
class Bar a b | a -> b
type FooCtx a b = ...
foo (Bar a b, FooCtx a b) => a -> a
but this defeats the purpose of grouping the constraints:
Until encountering this case, I assumed that Constraint synonyms could be blindly substituted for arbitrary constraint lists. The only other way I know to encapsulate constraints like this is with a class, but it suffers from the same problem: class (A a, B b, C c, ...) => FooCtx abc can't have any hidden types on the LHS. Is there some other way I might be able to fully gather all of these constraints?
You are misunderstanding how type variables are bound. They are not bound by the tau type (the a -> a in your example), but an implicit binder based on the full phi type ( (Bar ab) => a -> a ). This binding can be made explicit with the ExplicitForAll GHC language extension.
In your example, when you write something like
foo :: (Bar a b) => a -> a
then the full sigma type, with explicit tyvar-binding spelled out, is the following (since in the implicit case, all tyvars from the phi type are bound here)
foo :: forall a b. (Bar a b) => a -> a
This means there is no problem in using a constraint alias the same way: if you have eg
type FooCtx a b = (Bar a b, Num a, Eq a)
then the following is a valid type signature:
foo' :: forall a b. (FooCtx a b) => a -> a
and thus, the following shorthand is valid as well:
foo' :: (FooCtx a b) => a -> a
This problem can be solved with TypeFamilies and FlexibleContexts .
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
We have three classes, A , B , and C and your original foo function.
class A a
class B a
class C a
foo :: (A a, B b, C c) => a -> b -> c
foo = undefined
The Bar class uses a type family to figure out what B goes with an a . I've added an additional function to it just to write the example foo' .
class Bar a where
type BofA a :: *
aToB :: a -> BofA a
foo' is a function that doesn't have any inputs or outputs that are B , but still uses foo in its implementation. It requires that the BofA type associated with a satisfy the B constraint. This signature requires flexible contexts.
foo' :: (A a, Bar a, B (BofA a), C c) => a -> a -> c
foo' x y = foo x (aToB y)
上一篇: 将字典变成约束
下一篇: 用fundeps捆绑约束