Re: Typing units correctly
On Wed, Feb 14, 2001 at 08:10:39AM -0800, Andrew Kennedy wrote: To be frank, the poster that you cite doesn't know what he's talking about. He makes two elementary mistakes: Quite right, I didn't know what I was talking about. I still don't. But I do hope to learn. (a) attempting to encode dimension/unit checking in an existing type system; We're probably thinking about different contexts, but please see the attached file (below) for a partial solution. I used Hugs' dependent types to get type inference. This makes me uneasy, because I know that Hugs' instance checking is, in general, not decidable; I don't know if the fragment I use is decidable. You can remove the dependent types, but then you need to type all the results, etc., explicitly. This version doesn't handle negative exponents; perhaps what you say here: As others have pointed out, (a) doesn't work because the algebra of units of measure is not free - units form an Abelian group (if integer exponents are used) or a vector space over the rationals (if rational exponents are used) and so it's not possible to do unit-checking by equality-on-syntax or unit-inference by ordinary syntactic unification. ... is that I won't be able to do it? Note that I didn't write it out, but this version can accomodate multiple units of measure. (b) not appreciating the need for parametric polymorphism over dimensions/units. ... Furthermore, parametric polymorphism is essential for code reuse - one can't even write a generic squaring function (say) without it. I'm not sure what you're getting at here; I can easily write a squaring function in the version I wrote. It uses ad-hoc polymorphism rather than parametric polymorphism. It also gives much uglier types; e.g., the example from your paper f (x,y,z) = x*x + y*y*y + z*z*z*z*z gets some horribly ugly context: f :: (Additive a, Mul b c d, Mul c c e, Mul e c b, Mul d c a, Mul f f a, Mul g h a, Mul h h g) = (f,h,c) - a Not that I recommend this solution, mind you. I think language support would be much better. But specific language support for units rubs me the wrong way: I'd much rather see a general notion of types with integer parameters, which you're allowed to add. This would be useful in any number of places. Is this what you're suggesting below? To turn to the original question, I did once give a moment's thought to the combination of type classes and types for units-of-measure. I don't think there's any particular problem: units (or dimensions) are a new "sort" or "kind", just as "row" is in various proposals for record polymorphism in Haskell. As long as this is tracked through the type system, everything should work out fine. Of course, I may have missed something, in which case I'd be very interested to know about it. Incidentally, I went and read your paper just now. Very interesting. You mentioned one problem came up that sounds interesting: to give a nice member of the equivalence class of the principal type. This boils down to picking a nice basis for a free Abelian group with a few distinguished elements. Has any progress been made on that? Best, Dylan Thurston module Dim3 where default (Double) infixl 7 *** infixl 6 +++ data Zero = Zero data Succ x = Succ x class Peano a where value :: a - Int element :: a instance Peano Zero where value Zero = 0 ; element = Zero instance (Peano a) = Peano (Succ a) where value (Succ x) = value x + 1 ; element = Succ element class (Peano a, Peano b, Peano c) = PeanoAdd a b c | a b - c instance (Peano a) = PeanoAdd Zero a a instance (PeanoAdd a b c) = PeanoAdd (Succ a) b (Succ c) data (Peano a) = Dim a b = Dim a b deriving (Eq) class Mul a b c | a b - c where (***) :: a - b - c instance Mul Double Double Double where (***) = (*) instance (Mul a b c, PeanoAdd d e f) = Mul (Dim d a) (Dim e b) (Dim f c) where (Dim _ a) *** (Dim _ b) = Dim element (a *** b) instance (Show a, Peano b) = Show (Dim b a) where show (Dim b a) = show a ++ " d^" ++ show (value b) class Additive a where (+++) :: a - a - a zero :: a instance Additive Double where (+++) = (+) ; zero = 0 instance (Peano a, Additive b) = Additive (Dim a b) where Dim a b +++ Dim c d = Dim a (b+++d) zero = Dim element zero scalar :: Double - Dim Zero Double scalar x = Dim Zero x unit = scalar 1.0 d = Dim (Succ Zero) 1.0 f (x,y,z) = x***x +++ y***y***y +++ z***z***z***z***z
Re: Revised numerical prelude, version 0.02
Tue, 13 Feb 2001 18:32:21 -0500, Dylan Thurston [EMAIL PROTECTED] pisze:
Here's a revision of the numerical prelude.
I like it!
class (Real a, Floating a) = RealFrac a where
-- lifted directly from Haskell 98 Prelude
properFraction :: (Integral b) = a - (b,a)
truncate, round :: (Integral b) = a - b
ceiling, floor :: (Integral b) = a - b
These should be SmallIntegral.
For an instance of RealIntegral a, it is expected that a `quot` b
will round towards minus infinity and a `div` b will round towards 0.
The opposite.
class (Real a) = SmallReal a where
toRational :: a - Rational
class (SmallReal a, RealIntegral a) = SmallIntegral a where
toInteger :: a - Integer
These two classes exist to allow convenient conversions, primarily
between the built-in types. These classes are "small" in the sense
that they can be converted to integers (resp. rationals) without loss
of information.
I find names of these classes unclear: Integer is not small integral,
it's big integral (as opposed to Int)! :-)
Perhaps these classes should be called Real and Integral, with
different names for current Real and Integral. But I don't have
a concrete proposal.
--
__(" Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/
^^ SYGNATURA ZASTPCZA
QRCZAK
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Revised numerical prelude, version 0.02
On Wed, Feb 14, 2001 at 09:53:16PM +, Marcin 'Qrczak' Kowalczyk wrote: Tue, 13 Feb 2001 18:32:21 -0500, Dylan Thurston [EMAIL PROTECTED] pisze: Here's a revision of the numerical prelude. I like it! I'd like to start using something like this in my programs. What are the chances that the usability issues will be addressed? (The main one is all the fromInteger's, I think.) class (Real a, Floating a) = RealFrac a where -- lifted directly from Haskell 98 Prelude properFraction :: (Integral b) = a - (b,a) truncate, round :: (Integral b) = a - b ceiling, floor :: (Integral b) = a - b These should be SmallIntegral. It could be either one, since they produce the type on output (it calls fromInteger). I changed it, on the theory that it might be less confusing. But it should inherit from SmallReal. (Oh, except then RealFloat inherits from SmallReal, which it shouldn't have to. Gah.) For an instance of RealIntegral a, it is expected that a `quot` b will round towards minus infinity and a `div` b will round towards 0. The opposite. Thanks. class (Real a) = SmallReal a where toRational :: a - Rational class (SmallReal a, RealIntegral a) = SmallIntegral a where toInteger :: a - Integer ... I find names of these classes unclear: Integer is not small integral, it's big integral (as opposed to Int)! :-) I agree, but I couldn't think of anything better. I think this end of the heirarchy (that inherits from Real) could use some more work. RealIntegral and SmallIntegral could possibly be merged, except that it violates the principle of not combining semantically disparate operations in a single class. Best, Dylan Thurston ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: Primitive types and Prelude shenanigans
| On Mon, Feb 12, 2001 at 02:38:25PM -0800, William Lee Irwin III wrote:
| I had in mind looking within the compiler, actually. Where in the
| compiler? It's a big program, it might take me a while to do an
| uninformed search. I've peeked around a little bit and not gotten
| anywhere.
|
| If anyone else is pursuing thoughts along the same lines as I
| am (and I
| have suspicions), TysWiredIn.lhs appears quite relevant to the set of
| primitive data types, though there is no obvious connection to the
| module issue (PrelBase.Bool vs. Foo.Bool). PrelMods.lhs
| appears to shed
| more light on that issue in particular. $TOP/ghc/compiler/prelude/ was
| the gold mine I encountered.
Perhaps I should add something here.
I'm very sympathetic to the idea of making it possible to do entirely
without the standard Prelude, and to substitute a Prelude of one's own.
The most immediate and painful stumbling block in Haskell 98 is that numeric
literals,
like 3, turn into (Prelude.fromInt 3), where "Prelude.fromInt" really means
"the fromInt from the standard Prelude" regardless of whether the standard
Prelude is imported scope.
Some while ago I modified GHC to have an extra runtime flag to let you
change
this behaviour. The effect was that 3 turns into simply (fromInt 3), and
the
"fromInt" means "whatever fromInt is in scope". The same thing happens for
- numeric patterns
- n+k patterns (the subtraction is whatever is in scope)
- negation (you get whatever "negate" is in scope, not
Prelude.negate)
(Of course, this is not Haskell 98 behaviour.) I think I managed to forget
to tell anyone of this flag. And to my surprise I can't find it any more!
But several changes I made to make it easy are still there, so I'll
reinstate
it shortly. That should make it easy to define a new numeric class
structure.
So much for numerics. It's much less obvious what to do about booleans.
Of course, you can always define your own Bool type. But we're going to
have to change the type that if-then-else uses, and presumably guards too.
Take if-then-else. Currently it desugars to
case e of
True - then-expr
False - else-expr
but your new boolean might not have two constructors. So maybe we should
simply assume a function
if :: Bool - a - a - a
and use that for both if-then-else and guards I wonder what else?
For example, can we assume that
f x | otherwise = e
is equivalent to
f x = e
That is, "otherwise" is a guard that is equivalent to the boolean "true"
value.
("otherwise" might be bound to something else if you import a non-std
Prelude.)
If we don't assume this, we may generate rather bizarre code:
f x y | x==y = e1
| otherwise = e2
===
f x y = if (x==y) e1 (if otherwise e2 (error "non-exhaustive
patterns for f"))
And we'll get warnings from the pattern-match compiler. So perhaps we
should
guarantee that (if otherwise e1 e2) = e1.
You may say that's obvious, but the point is that we have to specify what
can be assumed about an alien Prelude.
Matters get even more tricky if you want to define your own lists.
There's quite a lot of built-in syntax for lists, and type checking that
goes with it. Last time I thought about it, it made my head hurt.
Tuples are even worse, because they constitute an infinite family.
The bottom line is this.
a) It's desirable to be able to substitute a new prelude
b) It's not obvious exactly what that should mean
c) And it may not be straightforward to implement
It's always hard to know how to deploy finite design-and-implementation
resources. Is this stuff important to a lot of people?
If you guys can come up with a precise specification for (b), I'll
think hard about how hard (c) really is.
Simon
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Scalable and Continuous
Marcin 'Qrczak' Kowalczyk wrote: I'm afraid of making too many small classes. But it would perhaps be not so bad if one could define superclass' methods in subclasses, so that one can forget about exact structure of classes and treat a bunch of classes as a single class if he wishes. It would have to be combined with compiler-inferred warnings about mutual definitions giving bottoms. I totally agree with this. We should be able to split up Num into many superclasses, while still retaining the traditional Num, and not inconveniencing anybody currently using Num. We could even put the superclasses into Library modules, so as not to "pollute" the standard Prelude's namespace. The Prelude could import those modules, then define Num and Num's instances, and only export the Num stuff. We shouldn't have to be afraid of making too many classes, if that more precisely reflects reality. It is only the current language definition that makes us afraid of this. We should be able to work with a class, subclass it, and define instances of it, without needing to know about all of its superclasses. This is certainly true in OOP, although I realize of course that OOP classes are not Haskell classes. I also wonder: should one be allowed to create new superclasses of an existing class without updating the original class's definition? Also, should the subclass be able to create new default definitions for functions in the superclasses? I think it should; such defaults would only be legal if the superclass did not define a default for the same function. What do you mean by mutual definitions? Matt Harden ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Scalable and Continuous
Wed, 14 Feb 2001 23:27:55 -0600, Matt Harden [EMAIL PROTECTED] pisze:
I also wonder: should one be allowed to create new superclasses of an
existing class without updating the original class's definition?
It would not buy anything. You could not make use of the superclass
in default definitions anyway (because they are already written).
And what would happen to types which are instances of the subclass
but not of the new superclass?
Also, should the subclass be able to create new default definitions
for functions in the superclasses?
I hope the system can be designed such that it can.
such defaults would only be legal if the superclass did not define
a default for the same function.
Not necessarily. For example (^) in Num (of the revised Prelude)
has a default definition, but Fractional gives the opportunity to
have better (^) defined in terms of other methods. When a type is an
instance of Fractional, it should always have the Fractional's (^)
in practice. When not, Num's (^) is always appropriate.
I had many cases like this when trying to design a container class
system. It's typical that a more specialized class has something
generic as a superclass, and that a more generic function can easily
be expressed in terms of specialized functions (but not vice versa).
It follows that many kinds of types have the same written definition
for a method, which cannot be put in the default definition in the
class because it needs a more specialized context.
It would be very convenient to be able to do that, but it cannot be
very clear design. It relies on the absence of an instance, a negative
constraint. Hopefully it will be OK, since it's determined once for a
type - it's not a systematic way of parametrizing code over negative
constrained types, which would break the principle that additional
instances are harmless to old code.
This design does have some problems. For example what if there are two
subclasses which define the default method in an incompatible ways.
We should design the system such that adding a non-conflicting instance
does not break previously written code. It must be resolved once per
module, probably complaining about the ambiguity (ugh!), but once
the instance is generated, it's cast in stone for this type.
What do you mean by mutual definitions?
Definitions of methods in terms of each other. Suppose there is a
class having only (-) and negate, with default definitions:
a - b = a + negate b
negate b = zero - b
When we make an instance of its subclass but don't make an explicit
instance of this class and don't write (-) or negate explicitly,
it would be dangerous if the compiler silently included definitions
generated by the above, because both are functions which always
return bottoms.
The best solution I can think of is to let the compiler deduce that
these default definitions lead to a useless instance, and give a
warning when both are instantiated from the default. It cannot be an
error because there is no formal way we can distinguish bad mutual
recursion from good mutual recursion. The validity of the code cannot
depend on heuristics, but warnings can. There are already warnings
when a method without default is not defined explicitly (although
people say it should be an error; it is diagnosable).
--
__(" Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/
^^ SYGNATURA ZASTPCZA
QRCZAK
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
