Skip to content

Explicit functional dependencies in constraint kinds #3078

Description

@kcsongor

It seems desirable to be able to talk about required fundeps for a given polymorphic constraint (when constraint kinds are implemented).

This would make it possible to do higher-order programming at the type-level, consider the example:

class Map
  (f :: (a :: Nat) -> (b :: Nat) -> Constraint | a -> b) -- <- here
  (xs :: List Nat)
  (out :: List Nat)
  | f xs -> out

If some sort of coverage condition were to be implemented for functional dependencies, this extension would make it possible for more instances to be accepted.

An important question raised by @LiamGoodacre is how to deal with requiring a -> b, but being given a -> b c, etc. I think these should be possible to work out in general by computing the transitive closure of the given dependencies and checking the required one is a member of that set -- but it needs more thought.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions