Re: [Haskell-cafe] Re: exceptions vs. Either

You should include the definitions of the classes before saying
HOrderedList l' just has to prove by induction that for any element in the list, the next element is greater, so the class is simply: class HOrderedList l instance HNil instance HCons a HNil instance (HOrderedList (HCons b l),HLe a b) => HCons a (HCons b l) which is the equivalent type level program to ordered :: [Int] -> Bool ordered [] = True ordered [a] = True ordered (a:(b:l)) = if a<=b then ordered (b:l) else False ordered _ = False It is obvious by observation that the a<=b ensures order. This is a lot simpler than say a heap-sort. I suppose you could contend that there are some classes above I still haven't defined - but you wouldn't expect to see definitions for (<=) which is defined in the prelude. Of course to show statically that order is preserved the 'value' of the elements to be ordered must be visible to the type system - so the values must be reified to types... This can be done for any Haskell type, but for numbers we would use Peano numbers - the HLe class for these is again easily defined by induction: class HLe n n' instance HLe HZero HZero instance HLe x y => HLe (HSucc x) (HSucc y) Keean.

On Fri, 2004-08-06 at 14:05, MR K P SCHUPKE wrote:
You should include the definitions of the classes before saying
HOrderedList l' just has to prove by induction that for any element in the list, the next element is greater, so the class is simply:
class HOrderedList l instance HNil instance HCons a HNil instance (HOrderedList (HCons b l),HLe a b) => HCons a (HCons b l)
Somewhat off-topic, It's when we write classes like these that closed classes would be really useful. You really don't want people to add extra instances to this class, it'd really mess up your proofs! I come across this occasionally, like when modelling external type systems. For example the Win32 registry or GConf have a simple type system, you can store a fixed number of different primitive types and in the case of GConf, pairs and lists of these primitive types. This can be modelled with a couple type classes and a bunch of instances. However this type system is not extensible so it'd be nice if code outside the defining module could not interfere with it. The class being closed might also allow fewer dictionaries and so better run time performance. It would also have an effect on overlapping instances. In my GConf example you can in particular store Strings and lists of any primitive type. But now these two overlap because a String is a list. However these don't really overlap because Char is not one of the primitive types so we could never get instances of String in two different ways. But because the class is open the compiler can't see that, someone could always add an instance for Char in another module. If the class were closed they couldn't and the compiler could look at all the instances in deciding if any of them overlap. So here's my wishlist item: closed class GConfValue v where ... Duncan

Duncan Coutts
closed class GConfValue v where
Hmm...doesn't --8<-- module Closed(foo) where class C a where foo = ... instance C ... --8<-- module Main where import Closed ...foo... --8<-- do what you want? You can only use existing instances of C, but not declare them (outside of the Closed module), IIUC. -ketil -- If I haven't seen further, it is by standing in the footprints of giants

Ketil Malde
Duncan Coutts
writes: closed class GConfValue v where
Hmm...doesn't
--8<-- module Closed(foo) where class C a where foo = ... instance C ... --8<-- module Main where import Closed ...foo... --8<--
do what you want? You can only use existing instances of C, but not declare them (outside of the Closed module), IIUC.
Ah, but now you cannot use (Closed t) => as a predicate in type signatures, and since you cannot write a partial signature, you must omit the signature altogether... Regards, Malcolm

On Fri, 2004-08-06 at 15:44, Malcolm Wallace wrote:
Hmm...doesn't
--8<-- module Closed(foo) where class C a where foo = ... instance C ... --8<-- module Main where import Closed ...foo... --8<--
do what you want? You can only use existing instances of C, but not declare them (outside of the Closed module), IIUC.
Ah, but now you cannot use (Closed t) => as a predicate in type signatures, and since you cannot write a partial signature, you must omit the signature altogether...
A similar non-solution is to export the class name but not the class methods, so you cannot defined them in other modules. However this doesn't help if there are default methods or no methods, you can still say: instance ClosedClass Foo Note the lack of 'where' keyword. Granted, for most classes this would stop other modules interfering but it doesn't give the optimisation opportunities or the better overlapping instance detection. Duncan

Malcolm Wallace
Ah, but now you cannot use (Closed t) => as a predicate in type signatures, and since you cannot write a partial signature, you must omit the signature altogether...
Hmm..yes, that would be a disadvantage. :-) -ketil -- If I haven't seen further, it is by standing in the footprints of giants

Malcolm Wallace wrote:
and since you cannot write a partial signature,
Can't we really? It seems `partial signature' means one of two things: - we wish to add an extra constraint to the type of the function but we don't wish to explicitly write the type of the function and enumerate all of the constraints - we wish to specify the type of the function and perhaps some of the constraints -- and let the typechecker figure out the rest of the constraints. Both of the above is easily possible, in Haskell98. In the first case, suppose we have a function
foo x = Just x
and suppose we wish to add an extra constraint (Ord x) but without specifying the full signature of the function. We just wish to add one constraint.
addOrd:: (Ord x) => x -> a addOrd = undefined
foo' x | False = addOrd x foo' x = Just x
Even a not-so-sufficiently smart compiler should be able to eliminate any traces of the first clause of foo' in the run code. So, the recipe is to define a function like `addOrd' (or like an identity), give it the explicit signature with the desired constraint, and then `mention' that function somewhere in the body of foo. Or, as the example above shows, prepend a clause of the form foo arg ... | False = addOrd arg ... In that case, the body of the function foo does not have to be changed at all. For the second case: suppose we wrote a function
bar a i = a ! i
and wish to give it a type signature *> bar:: Array i e -> i -> e But that won't work: we must specify all the constraints: Could not deduce (Ix i) from the context () arising from use of `!' at /tmp/d.lhs:207 Probable fix: Add (Ix i) to the type signature(s) for `bar' In the definition of `bar': bar a i = a ! i But what if we wish to specify the type without the constraints (and let the compiler figure the constraints out)? Again, the same trick applies:
barSig:: Array i e -> i -> e barSig = undefined
bar' a i | False = barSig a i bar' a i = a ! i
Incidentally, barSig plays the role of a Java interface of a sort. barSig is a bona fide function, and can be exported and imported. To make sure that some other function baz satisfies the barSig interface (perhaps with a different set of constraints), all we need to do is to say baz arg1 ... | False = barSig arg1 ... We can also attach to barSig some constraints. The typechecker will figure out the rest, for bar' and baz.
participants (5)
-
Duncan Coutts
-
Ketil Malde
-
Malcolm Wallace
-
MR K P SCHUPKE
-
oleg@pobox.com