Alle Typparameter in funktionalen Abhängigkeiten voneinander abhängig

Question

Nehmen wir an, ich habe eine Typklasse mit n Typ Parameter und ich möchte, dass jeder von ihnen eindeutig alle anderen bestimmen. Genügt es, die Abhängigkeiten zu machen wie einen Zyklus bilden in

class Foo a b c | a -> b, b -> c, c -> a 

(linear), wo es einen Pfad von jedem Parameter zu jedem anderen, oder muss ich alle möglichen Pfade erweitern wie in

class Bar a b c | a -> b, a -> c, b -> a, b -> c, c -> a, c -> b 

(quadratisch)? Gibt es einen erkennbaren Unterschied zwischen den beiden? Und wie wäre es

class Baz a b c | a -> b c, b -> a c, c -> a b 

Answer 1

Operativ alle oben sind äquivalent:

Zunächst einmal ist a -> b c wahrsten Sinne des Wortes das gleiche wie a -> b, a -> c.

Als nächstes nehmen wir an, Foo a b c => (a, b, c). Sagen wir, wir realisieren das a ~ A. Wir finden die a -> b fundep und durchsuchen Instanzen nach b ~ B. Wieder finden wir die b -> c fundep und realisieren c ~ C. Voila wir haben (A, B, C).

Wenn wir stattdessen Bar a b c => (a, b, c) mit a ~ A hätten, würden wir a -> b gefunden haben, und b ~ B jedoch vor b -> c zu finden, würden wir a -> c gefunden haben.

Der einzige Unterschied besteht darin, welche fundep-Pfeile verwendet werden, um auf die Typen zu schließen. a -> b, b -> c und a -> b, a -> c können nicht zu unterschiedlichen Ergebnissen führen.