[Haskell-cafe] Functional dependencies and Peano numbers

TIMOTHY MICHAEL CARSTENS t.carstens at utah.edu
Tue Jul 6 17:18:39 EDT 2010

```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

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
> _______________________________________________