Functional dependencies and Peano numbers
Hi, there is a lot of buzz around functional dependencies on the mailing list and Planet Haskell. I've read some of the tutorials and I think I understand how they work but I still haven't figured out where they can be useful. * Can someone give me a real world (preferably hackagedb) example where functional dependencies are used? * Can someone give me a real world (preferably hackagedb) example where Peano numbers a la "data Zero; data Succ n" are used? Finally... * All the examples involving functional dependencies are on the form
a b c | a b -> c
but can they also be on a form similar to
a b c d e f g h| b c -> d e f | b d g -> h
(i.e. d,e,f are decided by the b,c-combination while h is decided by the b,d,g-combination)? -- Oscar
Here's some code that uses them: http://gist.github.com/465918 This is a program that uses 4th-order Runge–Kutta to simulate some physics. It keeps track of units of measurement as it does its work. To do this, it uses type-level Peano numerals: every physical quantity in this program is expressed as a product of seconds, meters, and kilograms. In other words, the physical units are tracked in the type system. This is tracked in the Physical data structure. The code shows how this can be used to model speed, acceleration, and force. I haven't looked at this code in a while, so it's possible some of the comments are slightly off :/ It uses type families instead of functional dependencies. Anecdotally, my experience has been that functional dependencies are much faster. You might find that it takes ghci a good deal of time to load this file; type checking the rk4 function seems to be expensive. Best, -Tim On Jul 6, 2010, at 1:37 PM, Oscar Finnsson wrote:
Hi,
there is a lot of buzz around functional dependencies on the mailing list and Planet Haskell. I've read some of the tutorials and I think I understand how they work but I still haven't figured out where they can be useful.
* Can someone give me a real world (preferably hackagedb) example where functional dependencies are used?
* Can someone give me a real world (preferably hackagedb) example where Peano numbers a la "data Zero; data Succ n" are used?
Finally...
* All the examples involving functional dependencies are on the form
a b c | a b -> c
but can they also be on a form similar to
a b c d e f g h| b c -> d e f | b d g -> h
(i.e. d,e,f are decided by the b,c-combination while h is decided by the b,d,g-combination)?
-- Oscar _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 7/6/10 15:37 , Oscar Finnsson wrote:
but can they also be on a form similar to
a b c d e f g h| b c -> d e f | b d g -> h
(i.e. d,e,f are decided by the b,c-combination while h is decided by the b,d,g-combination)?
I think the answer to this is "yes, but if you have an MPTC with 8 parameters then you desperately need to refactor". - -- brandon s. allbery [linux,solaris,freebsd,perl] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkwz7bkACgkQIn7hlCsL25Vk+gCfcfeYYRtUaS/y28P9V852EUVt GnMAn0ACdIoW5iT+XVfOFXFLCxFzYomr =aujb -----END PGP SIGNATURE-----
Brandon S Allbery KF8NH wrote:
On 7/6/10 15:37 , Oscar Finnsson wrote:
but can they also be on a form similar to
a b c d e f g h| b c -> d e f | b d g -> h (i.e. d,e,f are decided by the b,c-combination while h is decided by the b,d,g-combination)?
I think the answer to this is "yes, but if you have an MPTC with 8 parameters then you desperately need to refactor".
Yes, you can add multiple dependencies. The syntax is to use , after the first |. While having eight parameters is surely a desperate need for refactoring, there are times when you'd want multiple dependencies. For example, you can say class F a b | a -> b, b -> a where... to express a bijective function on types (that is, for every pair of A and B, if you know one of them then you know what the other must be uniquely). -- Live well, ~wren
On Sat, Jul 10 2010, wren ng thornton wrote: [...]
Yes, you can add multiple dependencies. The syntax is to use , after the first |.
While having eight parameters is surely a desperate need for refactoring, there are times when you'd want multiple dependencies. For example, you can say
class F a b | a -> b, b -> a where...
to express a bijective function on types (that is, for every pair of A and B, if you know one of them then you know what the other must be uniquely).
I know i should read the relevant articles, but how would one express such a bijection using type families? TIA, jao -- You err by thinking simplicity and elegance are mostly cosmetic. Simplicity and elegance are overwhelmingly practical virtues. - William D Clinger, comp.lang.scheme
On Sun, Jul 11, 2010 at 12:43:47AM +0200, Jose A. Ortega Ruiz wrote:
On Sat, Jul 10 2010, wren ng thornton wrote:
[...]
Yes, you can add multiple dependencies. The syntax is to use , after the first |.
While having eight parameters is surely a desperate need for refactoring, there are times when you'd want multiple dependencies. For example, you can say
class F a b | a -> b, b -> a where...
to express a bijective function on types (that is, for every pair of A and B, if you know one of them then you know what the other must be uniquely).
I know i should read the relevant articles, but how would one express such a bijection using type families?
You would just create two type families, one for each direction of the mapping: type family F1 a :: * type instance F1 Int = Bool type instance F1 ... type family F2 a :: * type instance F2 Bool = Int type instance F2 ... Of course, this is not quite the same thing, since with the MPTC version we are guaranteed to get a bijection, but there is nothing forcing F1 and F2 to have anything to do with one another (for example I could have written type instance F2 Char = Int). But I don't know whether this would make a difference in practice. -Brent
participants (6)
-
Brandon S Allbery KF8NH -
Brent Yorgey -
Jose A. Ortega Ruiz -
Oscar Finnsson -
TIMOTHY MICHAEL CARSTENS -
wren ng thornton