Haskell: esempi non ovvi di dipendenze funzionali

Question

Gli esempi di dipendenze funzionali che ho visto si riducono alla mappatura container -> element e arguments -> result (come in Mult Matrix Vector Vector). Sembrano essere meglio espressi con funzioni di tipo. Nella teoria dei database vengono considerate relazioni più complesse che non sono di questo tipo (come a -> b, b -> a).

Esistono esempi di utilizzo di FD in Haskell che non possono essere scritti correttamente utilizzando le funzioni di tipo?

Answer 1

Come già affermato da Heinrich Apfelmus, MPTC + FunDeps e TF sono equivalenti. Le differenze sorgono quando sono combinate con altre estensioni, in particolare con istanze sovrapposte. Le TF non sono corrette quando è consentita la sovrapposizione mentre FunDeps consente la sovrapposizione. Ad esempio è facile implementare l'uguaglianza dei tipi con FunDeps:

data HTrue 
data HFalse 

class TypeEq a b eq | a b -> eq 
instance    TypeEq a a HTrue 
instance eq ~ HFalse => TypeEq a b eq 

Qui il punto chiave si sovrappone. In linea di principio è possibile implementare l'uguaglianza di tipo senza sovrapposizioni, ma richiederà il supporto del compilatore. Tale approccio è descritto da Oleg qui: http://okmij.org/ftp/Haskell/typeEQ.html

P.S. C'era lengthy discussion sulla mailing list haskell-prime su questo argomento.

Answer 2

Come Manuel Chakravarty explains, le funzioni di tipo e le dipendenze funzionali hanno all'incirca la stessa espressività, è possibile tradurre una formulazione nell'altra. Iniziano a differire solo quando guardi all'interazione con altre estensioni di lingua come GADT o UndecidableInstances. Considero che le famiglie di tipo sono attualmente favorite per l'implementazione in GHC perché la loro interazione con GADT e tipi esistenziali è sostanzialmente più semplice.