[Haskell-cafe] Functional dependencies and Peano numbers

[TIMOTHY MICHAEL CARSTENS]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe