Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proposal: Named functional dependencies #3580

Open
paf31 opened this issue Mar 29, 2019 · 17 comments

Comments

Projects
None yet
6 participants
@paf31
Copy link
Member

commented Mar 29, 2019

Computing large types using functional dependencies leads to a problem:

class C a b | a -> b where
  build :: Proxy a -> b

If I want to have my class C build a value of type b for me, then I can either give a type annotation (cumbersome for large types and prone to breakage), or give it a type like

built :: forall b. C A b => b
built = build (Proxy :: Proxy A)

but that approach leads to the dictionary for C A b being inlined at every call site, which is inefficient at runtime.

I'd like to propose we add named functional dependencies as a way to refer to the computed type instead.

Proposed Syntax

class C a b
  | Computed :: a -> b

This would act like a type synonym which would only be defined for types with an instance.

Now I can give a much nicer type annotation which has neither of the problems above:

built :: Computed A
built = build (Proxy :: Proxy A)

This essentially turns functional dependencies into associated types.

What do people think of this idea?

Notes

I think it could be possible to implement any necessary breaking changes early, such as

  • Removing syntactic support for multiple outputs in a functional dependency
  • Making names required (debatable)
@garyb

This comment has been minimized.

Copy link
Member

commented Mar 29, 2019

I like it. What do you see as the advantages of this, over "just" implementing associated types?

@paf31

This comment has been minimized.

Copy link
Member Author

commented Mar 29, 2019

I'd think this is probably the simplest path to something which gives the same benefits as associated types, and implementing them separately would be like having two features which do most of the same things.

It mostly comes down to syntax though. You could perhaps dress up functional dependencies with associated type syntax, but with all of the same constraints.

Incidentally, there is a bug in the functional dependencies check which is relevant here. It's possible to write something like

instance c :: C A (B x)

where x is a type variable mentioned in b but not in a. This violates the functional dependency condition.

This would be detected if we wrote this as a pseudo type synonym:

type Computed a
type instance Computed A = B x -- x not in scope here
@parsonsmatt

This comment has been minimized.

Copy link
Contributor

commented Mar 29, 2019

I believe there's a paper on something like this. I'll try and find it

@paf31

This comment has been minimized.

Copy link
Member Author

commented Mar 29, 2019

I believe there's a paper on something like this. I'll try and find it

The original "Type Classes with Functional Dependencies" paper by Mark Jones talks about this idea in section 7 near the end.

@parsonsmatt

This comment has been minimized.

Copy link
Contributor

commented Mar 29, 2019

I was thinking of Language and Program Design for Functional Dependencies
, section 3 "Functional Notation"

@garyb

This comment has been minimized.

Copy link
Member

commented Mar 29, 2019

How would you see this working for something like Prim.Row.Union or Prim.Row.Cons where there's multiple different sets of dependencies for the same vars? Just as they are now but naming each one:

class Union (left :: # Type) (right :: # Type) (union :: # Type) 
  | UBoth :: left right -> union
  , ULeft :: right union -> left
  , URight :: union left -> right

Something like that?

@paf31

This comment has been minimized.

Copy link
Member Author

commented Mar 29, 2019

Yes, exactly. Maybe in that case they could be called something like Append, UnappendL and UnappendR.

@garyb

This comment has been minimized.

Copy link
Member

commented Mar 29, 2019

Yeah, those names make sense - I was just wondering about the mechanics of dealing with multiple dependencies.

@natefaubion

This comment has been minimized.

Copy link
Contributor

commented Mar 29, 2019

I think for syntax the :: seems unnecessary, Append left right -> union seems reasonable enough. I find :: combined with left right -> union to be really odd, since it seems like you are applying right to left. Does this implicitly propagate constraints? How does it work with type aliases? I always found the functional notation in that paper rather confusing, personally, and I don't think I've seen it implemented anywhere.

@natefaubion

This comment has been minimized.

Copy link
Contributor

commented Mar 29, 2019

To me, it seems like the most straightforward way to implement this would be as a desugaring step (float out to the "real" constraint and deduplicate), but if that were the case, then your example would necessarily desugar into what you would write today, which requires a dictionary. If it's not a desugaring step, I think you'll be on your way to implementing type families 😄. I'm happy to be corrected, but this doesn't seem like just a syntactic issue.

@paf31

This comment has been minimized.

Copy link
Member Author

commented Mar 29, 2019

Why would it need a dictionary, as opposed to simply knowing an instance exists?

@paf31

This comment has been minimized.

Copy link
Member Author

commented Mar 29, 2019

As for syntax, what about Append left right = union, since we really want the type expression on the left to be a valid replacement anywhere you'd mention union?

@natefaubion

This comment has been minimized.

Copy link
Contributor

commented Mar 29, 2019

Why would it need a dictionary, as opposed to simply knowing an instance exists?

This is the part that doesn't make sense to me, but I'm having a hard time articulating why. In the paper, it's suggested that functional notation be expanded to the constraint you'd normally write, but we don't want that since it results in a dictionary. Are you suggesting this notation only applies when all arguments have no type variables?

@paf31

This comment has been minimized.

Copy link
Member Author

commented Mar 29, 2019

When you write an instance, the mapping from named fundeps to their classes has to be stored in some global lookup. Then, during type synonym expansion, if we see a "synonym" in that lookup, i.e. one from one of these associated types, we find the relevant instance using the usual logic from the elaborator and then expand the synonym using the functional dependency. That doesn't need a dictionary, because it's purely at the level of types, not values.

Edit: technically, more is necessary, since we might not have the type information necessary to apply the "usual logic" at the point of synonym expansion. However, we can hopefully expand it to a placeholder which can be replaced during the usual solve-unify loop, just like we do with dictionaries. But this would be a placeholder for a type, not for a value.

@natefaubion

This comment has been minimized.

Copy link
Contributor

commented Mar 29, 2019

Does this then only apply to classes/instances that have no runtime evidence?

technically, more is necessary, since we might not have the type information necessary to apply the "usual logic" at the point of synonym expansion. However, we can hopefully expand it to a placeholder which can be replaced during the usual solve-unify loop, just like we do with dictionaries. But this would be a placeholder for a type, not for a value.

This sounds an awful lot like type families to me 😄.

@hdgarrood

This comment has been minimized.

Copy link
Member

commented Mar 31, 2019

I don't think efficiency is a strong enough reason to add a type system feature like this for me, personally, especially not if it involves breaking changes. I think I might prefer providing a way of asking the compiler to generate specialised versions of values which have constraints.

@timjs

This comment has been minimized.

Copy link

commented Apr 23, 2019

I really like this idea! Why not demand writing all functional dependencies in the form of associated types like this:

class C a b where
  type Computed a = b

In the body of the class, every functional dependency would be written out explicitly in the form of an associated type (or "associated type dependency", if you like...). It can only use the variables declared with the class. Using this notation, it is possible to write down all possible relations between types:

-- Open relations:
class Cast a b where  -- Nothing special here
  cast :: a -> b

-- Surjective relations:
class Collection c e where
  type Elem c = e   -- Like the old `| c -> e`
  empty  :: c
  insert :: e -> c -> c
  member :: e -> c -> Bool

-- Bijective relations
class Boxed b u where
  type Unbox b = u
  type Box   u = b  -- Like the old `| b -> u, u -> b`
  unbox :: b -> u
  box   :: u -> b

-- Multiple type arguments:
class Add' (a :: Nat) (b :: Nat) (r :: Nat) where
  type Add a b = r  -- Like the old `| a b -> r`

-- Multiple type results:
class FiniteMap m i e where
  type Index m = i
  type Elem  m = e  -- Like the old `| m -> i e`
  empty  :: m
  lookup :: i -> m -> Maybe e
  extend :: i -> e -> m -> m

I think it would create a best of both worlds. From type families:

  • Named associated types are less cryptic than functional dependencies.
  • Associated types can be used in type signatures (roughly section 3 of [2]):
    append :: Vect n a -> Vect m a -> Vect (Add n m) a
    -- instead of
    append :: Add' n m k => Vect n a -> Vect m a -> Vect k a

From functional dependencies:

  • Reuse the existing machinery on functional dependencies.
  • Automatically instantiate associate types when instantiating the class, so no repetitive typing:
    instance (Eq i) => FiniteMap (i -> e) i e where ...
      -- Gives `Index (i -> e) = i` and `Elem (i -> e) = e`
    instance FiniteMap (Array e) Int e where ...
      -- Gives `Index (Array e) = Int` and `Elem (Array e) = e`
    instance FiniteMap BitSet Int Bool where ...
      -- Gives `Index BitSet = Int` and `Elem BitSet = Bool`
  • No need for equality constraints (see section 3.3 of [2]):
    insertInt :: Collection c Int => c -> c
    -- instead of
    insertInt :: (Collects c, Elem c ~ Int) => c -> c

Only nitpick: no functional syntax while defining associated types...

-- need to type
class And' (a :: Boolean) (b :: Boolean) (r :: Boolean) where
  type And a b = r

instance And' True  b b
else     And' False b False
else fail

-- instead of
type And (a :: Boolean) (b :: Boolean) :: Boolean where
  And True  b = b
  And False b = False

(Could be added as sugar, but I'm not sure if there are really great benefits in doing that. Although Jones and Diatchki [2] state in section 3.5 that type synonyms are actually a special case of functional dependencies.)

[1] Jones, M. P. (2000). Type classes with functional dependencies. ESOP (pp. 230-244). Springer, Berlin.
[2] Jones, M. P., & Diatchki, I. S. (2009). Language and program design for functional dependencies. ACM SIGPLAN Notices, 44(2), 87–98. https://doi.org/10.1145/1543134.1411298

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.