3 ms·

One thing that often comes up in these discussions is using types to manage units of measure. I think this is an awesome example, so here's a sample of my favor

by tikhonj 13y ago

One thing that often comes up in these discussions is using types to manage units of measure. I think this is an awesome example, so here's a sample of my favorite library for it (unittyped)[1]: *Main> (1 meter / second) * 5 second 5.0 m/s⋅s *Main> 2 meter + (1 meter / second) * 5 second 7.0 m One really cute trick is that the various si prefixes are actually functions. So instead of defining every combination of milli-, centi-, deci and so on, you can write them like this: Main*> 1 kilo meter + 324 centi meter 1.00324 km The library can convert between compatible units automatically, so you never have to worry about the conversion factor: Main*> 1.23 kilo meter `as` mile 0.7642865664519207 mile Since the prefixes are systematic, you can come up with your own bastardized units: Main*> 1 centi mile `as` kilo inch 0.6336000000000002 kin Of course, if we try to combine incompatible units, we get a type error. And this shows the most glaring problem with this library :P. Main*> 10 second + 2 inch <interactive>:38:11: Couldn't match type 'GHC.Types.False with 'GHC.Types.True When using functional dependencies to combine UnitTyped.And 'GHC.Types.False 'GHC.Types.False 'GHC.Types.False, arising from the dependency `a b -> c' in the instance declaration in `UnitTyped' UnitTyped.And 'GHC.Types.False 'GHC.Types.False 'GHC.Types.True, arising from a use of `+' at <interactive>:38:11 In the expression: 10 second + 2 inch In an equation for `it': it = 10 second + 2 inch This message is absolutely hideous. But it's still better than nothing. I think some mechanism for letting libraries customize type error messages would be awesome, but I don't know what that would look like. [1]: https://bitbucket.org/xnyhps/haskell-unittyped/wiki/Examples https://bitbucket.org/xnyhps/haskell-unittyped/wiki/Examples

softbuilder 13y ago
You may enjoy Frink[1] if you haven't encountered it yet. [1] http://futureboy.us/frinkdocs/ http://futureboy.us/frinkdocs/
johnbender 13y ago
The difficulty with type errors partly arises out of inference. The program assumes NOTHING about the type of the expressions and instead collects constraints as it descends into sub-expressions. Once it has finished collecting constraints for the all the sub-expressions it attempts to satisfy those constraints. If the constraints can't be satisfied there are two problems. First, you have to know where you got the constraint from. This is fairly easy to solve in implementation you can tag the constraints for example. Second, is that the way in which the constraint "fails" or is unsatisfiable doesn't always give you enough information. For example: \x -> if x then x else 1 Here the constraints basically say that x has type Bool and 1 has type Int. This is obviously wrong because the `if x then x else 1` has to be either Bool or Int. Now the question is, which one is wrong? Is the use of the second x wrong or is the use of the 1 wrong. You can't know so you have to report something and this is only a trivial example. [edit]: I said "mostly" but I changed that to be "partly" because type systems like Haskell's are very complex and in some cases type inference is undecideable (rank n polymorphism) so that obviously makes reporting an error very hard :)

by tikhonj 13y ago

softbuilder 13y ago

You may enjoy Frink[1] if you haven't encountered it yet. [1] http://futureboy.us/frinkdocs/ http://futureboy.us/frinkdocs/

johnbender 13y ago

The difficulty with type errors partly arises out of inference. The program assumes NOTHING about the type of the expressions and instead collects constraints as it descends into sub-expressions. Once it has finished collecting constraints for the all the sub-expressions it attempts to satisfy those constraints. If the constraints can't be satisfied there are two problems. First, you have to know where you got the constraint from. This is fairly easy to solve in implementation you can tag the constraints for example. Second, is that the way in which the constraint "fails" or is unsatisfiable doesn't always give you enough information. For example: \x -> if x then x else 1 Here the constraints basically say that x has type Bool and 1 has type Int. This is obviously wrong because the `if x then x else 1` has to be either Bool or Int. Now the question is, which one is wrong? Is the use of the second x wrong or is the use of the 1 wrong. You can't know so you have to report something and this is only a trivial example. [edit]: I said "mostly" but I changed that to be "partly" because type systems like Haskell's are very complex and in some cases type inference is undecideable (rank n polymorphism) so that obviously makes reporting an error very hard :)