Re: [Haskell] Eliminating Array Bound Checking through Non-dependent types
( A really interesting post on static elimination of array bounds checking by Oleg...) Some questions and suggestions: What is the relation to the sized types by Lars Pareto and John Hughes? What is the relation to classical range analyses for (e.g.) array index expressions, which have been known for a long time for imperative languages? A program analysis like range analysis is not exact, of course: it must make safe approximations sometimes and will sometimes say that an array index might be out of bounds when it actually won't. In your framework, this seems to correspond to the fact that you must verify your propositions about index expressions. If the formulae fall into some decidable category, then they can be verified automatically, otherwise an automatic method based on your framework will have to give up sometimes, just like a conventional program analysis. The formulae you give in your example are all Presburger formulae, for which there are decision procedures, and you could use a public domain Presburger solver like the Omega Test by Bill Pugh. Have you though of this possibility? Björn Lisper ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Eliminating Array Bound Checking through Non-dependent types
Hello Oleg, hello all I agree with you on this: [EMAIL PROTECTED] wrote: There is a view that in order to gain static assurances such as an array index being always in range or tail being applied to a non-empty list, we must give up on something significant: on data structures such as arrays (to be replaced with nested tuples), on general recursion, on annotation-free programming, on clarity of code, on well-supported programming languages. That does not have to be the case. However, anyone who would argue (and I'm not saying you do) that work to try to make more advanced type systems and stronger static guarantees more convenient and `well-supported' is not necessary because it happens to be possible to bang out this or that example in Haskell as it stands if you think about it hard enough, is adopting the position of the ostrich. Of course, there might be other, better reasons why, in particular, dependently typed programming might turn out to be unrealistic: if anybody finds them, I'll give up. But, Oleg,... This message shows a non-trivial example involving native Haskell arrays, index computations, and general recursion. All arrays indexing operations are statically guaranteed to be safe -- and so we can safely use an efficient unsafeAt provided by GHC seemingly for that purpose. ...here you go too far for two reasons (1) What's a static guarantee? The safety is based on: Haskell type system, quantified type variables, and a compact general-purpose trusted kernel. What if I don't trust your kernel? The guarantees you require of your kernel are not statically checked. What guarantee do I have that the propositions which you identify are even the ones which are really needed to eliminate bounds checking? How does the machine replace ! by unsafeAt reliably, all by itself? Yes, you can convince _me_ that something of the sort will do, because I can follow the math. But what is the mechanism? What is the evidence? What's the downloadable object that can be machine-checked to satisfy my paranoid insurance company? Our example is `bsearch', taken from the famous paper Eliminating Array Bound Checking Through Dependent Types by Hongwei Xi and Frank Pfenning (PLDI'98). Hongwei Xi's code was written in SML extended with a restricted form of dependent types. Here is the original code of the example (taken from Figure 3 of that paper, see also http://www-2.cs.cmu.edu/~hwxi/DML/examples/) Hongwei Xi's code contains the evidence I'm asking for. The verification conditions are added by hand in the program as annotations, just as yours are annotations outside the program. His are checked by Presburger arithmetic, just as yours could be. [..] (2) And I hate to be a smartass, but... bbounds:: (Ix i) = BArray s i a - (BIndex s i, BIndex s i) bbounds (BArray a) = let (l,h) = bounds a in (BIndex l, BIndex h) Proposition: the two indices returned by bbounds are within the range of the array 'a'. Proof: from the semantics of the function `bounds', taken here as an axiom. ...this proposition is false. The bounds function returns bounds which are outside the range of the array when the array is empty. You'll notice that Hongwei Xi's program correctly handles this case. Don't get me wrong: I think your branded arrays and indices are a very good idea. You could clearly fix this problem by Maybe-ing up bbounds or (better?) by refusing to brand empty arrays in the first place. My point is merely this: if your guarantees really were static, you'd have fixed this bug already. Cheers Conor ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] image writing library
Oops. Lest anybody should copy it blindly: mkpgm :: Array (Int,Int) Int - String mkpgm cm = header ++ \n ++ image where header = unwords [P2,show width,show heigth,show maxval] image = unlines $ map show $ elems cm - (width,heigth) = snd $ bounds cm + (heigth,width) = snd $ bounds cm maxval = maximum (elems cm) -kzm -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Eliminating Array Bound Checking through Non-dependent types
In article [EMAIL PROTECTED], Bjorn Lisper [EMAIL PROTECTED] wrote: ( A really interesting post on static elimination of array bounds checking by Oleg...) Some questions and suggestions: Am I right suspecting, that this method also solves the problem of assuring the right p in p-modular arithmetic (as complained by Sergei Mechveliani in his Basic Algebra proposal)? -- Dipl.-Math. Wilhelm Bernhard Kloke Institut fuer Arbeitsphysiologie an der Universitaet Dortmund Ardeystrasse 67, D-44139 Dortmund, Tel. 0231-1084-257 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] image writing library
Ketil Malde wrote: I discovered that although XPM accepts values in the range 0x00..0xff, it is still monochrome. XGM (plain, that is, not raw) is approximately the same format, but displays the way I wanted. So I ended up using: mkpgm :: Array (Int,Int) Int - String mkpgm cm = header ++ \n ++ image where header = unwords [P2,show width,show heigth,show maxval] This may not work for many programs which read PGM files. The header is usually split into multiple lines, e.g. P2 256 256 255 Some programs may accept arbitrary whitespace between tokens, but others may insist upon newlines, e.g.: mkpgm cm = header ++ image where header = unlines $ map unwords [[P2],[show width, show height],[show maxval]] Also: (width,heigth) = snd $ bounds cm This assumes that fst $ bounds cm == (1,1). Not *very* beautiful, but seems to do the job for my stuff. I'll try the PPM library if I need something a tad more fancy - like colors :-) Writing PPM is only marginally more complex, e.g.: mkppm :: Array (Int,Int) (Int, Int, Int) - String mkppm cm = header ++ image where header = unlines $ map unwords [[P3],[show width, show height],[show maxval]] image = unlines $ map showRGB $ elems cm width = x1 - x0 + 1 height = y1 - y0 + 1 ((x0,y0),(x1,y1)) = bounds cm maxval = maximum $ concatMap unRGB (elems cm) showRGB (r,g,b) = unwords [show r, show g, show b] unRGB (r,g,b) = [r,g,b] -- Glynn Clements [EMAIL PROTECTED] ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Eliminating Array Bound Checking through Non-dependent types
Hello! What if I don't trust your kernel? The guarantees you require of your kernel are not statically checked. What guarantee do I have that the propositions which you identify are even the ones which are really needed to eliminate bounds checking? How does the machine replace ! by unsafeAt reliably, all by itself? Yes, you can convince _me_ that something of the sort will do, because I can follow the math. But what is the mechanism? What is the evidence? What's the downloadable object that can be machine-checked to satisfy my paranoid insurance company? That is very well said! I hope that you can forgive me if I reply by quoting the above two paragraphs back to you, with the substitution s/kernel/compiler/. What if I don't trust your compiler? I have heard a similar question asked of J. Strother Moore and J. Harrison. J. Strother Moore said that most of ACL2 is built by bootstrapping, from lemmas and strategies that ACL2 itself has proven. However, the core of ACL2 just has to be trusted. ACL2 has been used for quite a while and so there is a confidence in its soundness. Incidentally, both NSA and NIST found this argument persuasive, when they accepted proofs by ACL2 as evidence of high assurance, in awarding Orange book A1 and IFIPS 140-1 ratings -- the highest security ratings -- to some products. Hongwei Xi's code contains the evidence I'm asking for. The verification conditions are added by hand in the program as annotations, just as yours are annotations outside the program. His are checked by Presburger arithmetic, just as yours could be. Actually, as far as the PLDI'98 paper is concerned, they specifically say they do not use the full Presburger arithmetics. Rather, they solve the constraints by Fourier variable elimination. Anyway, even if the various elaboration and decision rules are proven to be sound and complete, what is the evidence that their implementation in the extended SML compiler is also sound and complete? Speaking of completeness, the procedure in PLDI'98 paper notes, Note that we have been able to eliminate all the existential variables in the above constraint. This is true in all our examples, but, unfortunately, we have not yet found a clear theoretical explanation why this is so. The conclusion specifically states that the algorithm is currently incomplete. ...this proposition is false. The bounds function returns bounds which are outside the range of the array when the array is empty. You'll notice that Hongwei Xi's program correctly handles this case. Don't get me wrong: I think your branded arrays and indices are a very good idea. You could clearly fix this problem by Maybe-ing up bbounds or (better?) by refusing to brand empty arrays in the first place. I have noticed that the branding trick would work very well with number-parameterized types. The latter provide missing guarantees, for example, statically outlaw empty arrays. Hongwei Xi's code has another neat example: a dot product of two arrays where one array is statically known to be no longer that the other. Number-Parameterized types can statically express that inequality constraint too. The Number-Parameterized types paper considers a more difficult example -- and indeed the typechecker forced me to give it a term that is verifiably a proof of the property (inequality on the sizes) stated in term's inferred type. The typecheker truly demanded a proof; shouting didn't help. Incidentally, the paper is being considered for JFP, I guess. I don't know if the text could be made available. I still can post the link to the code: http://pobox.com/~oleg/ftp/Haskell/number-param-vector-code.tar.gz I should emphasize that all proper examples use genuine Haskell arrays rather than nested tuples. Yet the type of the array includes its size, conveniently expressed in decimal notation. One can specify arithmetic equality and inequality constraints on the sizes of the array, in the type of the corresponding functions. The constraints can be inferred. One example specifically deals with the case when the sizes of those arrays are not known until the run-time -- moreover, change in the course of a computation that involves general recursion. It seems that branding trick nicely complements number-parameterized arrays and makes `dynamic' cases easier to handle. You'll notice that Hongwei Xi's program correctly handles this case. But what if I specified the dependent type with a mistake that overlook the empty array case? Would the dependent ML compiler catch me red-handed? In all possible cases? Where is the formal proof of that? I have failed to emphasize the parallels between Hongwei Xi's annotations and the corresponding Haskell code. What Hongwei Xi expressed in types, the previously posted code expressed in terms. The terms were specifically designed in such a way so that consequences of various tests were visible to the type systems, and so the corresponding
[Haskell-cafe] Re: exceptions vs. Either
After all, Java basically does exactly what you're asking for with Java's head/tail would be doing runtime checks if they are throwing exceptions, static guarantees mean the program would not be allowed to compile if it broke the static guarantees. end-programmers have to worry much less about handling errors properly. Which is a bad thing! All programmers always have to consider error conditions, if they don't they write buggy code - that's the nature of the beast. I prefer making programmers expicitly face the decisions they are making, rather than have things implicitly handled in a way that hides what is going on from the programmer. Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
After all, Java basically does exactly what you're asking for with Java's head/tail would be doing runtime checks if they are throwing exceptions, static guarantees mean the program would not be allowed to compile if it broke the static guarantees. Not so. In Java, the programmer is forced to handle most exceptions by the type system. That is, if the exception is not handled, the program will not compile, thus providing a static guarantee that exceptions are handled. Only unchecked exceptions (RuntimeException and Error) are exempt from this check. --KW 8-) ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
Not so. In Java, the programmer is forced to handle most exceptions I forgot you had to do that... Exceptions are explicit in the type signatures. I think Oleg posted a message a while back about how to make exceptions explicit in haskell type signatures... But I would rather use static guarantees where possible, and exceptions where necessary. I haven't really tried using the techniques for explicit exceptions, but on consideration I might see if it is practical to code in that style... Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
Static guarantees are great, but if you have to explicitly change your style of coding to cope with those extra constraints, it can become (very) cumbersome. I had to change coding style moving from imperative to declarative languages, but I think it was worth it... Likewise I think having the ability to make strong static guaranees is worth it - you may not, which is why it is important not to break any existing programs with language extensions (if any are necessary). My programs will have less bugs though! worse-is-better, even in its strawman form, has better survival I fully subscribe to the 'worse is better' approach, but I don't see how it contradicts the principle of static guarantees - you can have both. Simplicity is about algorithmic complexity not about whether type signatures are provided by the programmer. Infact type signatures are in themselves an embodyment of the simple is better principle. A type signature expresses certain static guarantees about the function in a vary compact way. Consider the sort example... being able to declare a type signature on a sort algorith that enforces ordering of the output would prove the sort algorithm can _only_ output correctly sorted lists under _all_ circunstances. This type signature is much simpler than the actual sort - hence is useful. sort :: (HList l,HOrderedList l') = l - l' Nice and readable, and much simpler than the actual algorithm (be it bubble sort, or a quick sort) Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
correctly sorted lists under _all_ circunstances. This type signature is much simpler than the actual sort - hence is useful. sort :: (HList l,HOrderedList l') = l - l' Nice and readable, and much simpler than the actual algorithm (be it bubble sort, or a quick sort) The type signature you give is no different from sort :: (C1 l, C2 l') = l - l' and conveys no more information. You should include the definitions of the classes before saying this is much simpler than the actual sort. --KW 8-) ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
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. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
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 ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] introspection | meta data
Can you name these fields? If so, haskell has (sorta clumsy) named
records,
and you can select and update fields by name, and you can replace
'setSFField 3 sf x' with 'sf {somefield=x}'
I did think of this, but unfortunatly my algorithm cant use names (without
hard coding all possible combinations )
So what is the general haskell approach to this type of
introspection/meta
data problem... ?
A C array of pointers maps closest to a MutableArray, which is mostly a
list
with different performance. Unless you're casting pointers, in which case
Dynamic types or the Generic stuff is maybe what you want. Or a redesign
;)
I looked at haskell arrays, but since I cant point to an element in my tuple
it wont work out. The ANSI C use of arrays is a really simple (but nasty)
way to provide a means for me to loop over a fixed struct record. The
Generic library looks super, only had time to browse some slides thus far,
but will defiantly try understand that.
As for a redesign and
Others have given good answers for this, but I suspect you may have chosen
the
wrong data structure...
I would be keen on any ideas you have on how to design this in haskell.
Learning to think in haskell is after all the goal :-) The example below is
trivial and real world, both reasons why I chose to use it.
Any comments welcome, none expected :-)
Thanks,
--
I idea is to perform a search over a number fields in a hierachical fashion
where each field can have a wild card. The real world example is printer
selection. In a multi-national company all users tend to be on one (or a
few) central servers, but require there printouts to come to them locally
whereever they are. Users typically range in 1000s and so by user
defintions are out.
Simplified Search fields:
Environemnt, Users, Report, Version, Host Printer
-- --
The most speicific field is host on the right with it becomming more
general moving to towards the left.
Setup data could choose to override all of report RPT1 version Ver1 to
Printer Bobs Printer
*ALL, *ALL, RPT1, Ver1, *ALL, Bobs Printer
but Simon may be an exception, then a record could be added like so:
*ALL, SIMON, RPT1, Ver1, *ALL, Simons Printer
This record would be found first for simon, but former found found for
everyone else.
A search starts from fully specific data i.e no wild cards.
The basic algortihm I worked out is:
1. Search setup data
2. If no record found
2a: Set current field to most specific field (host in this case)
2b: Toggle current field ( if Wildcard then make it value, if value make
it wildcard )
2c: if current field is *ALL goto 1 above (we stop here to perform a
search on the current permutation)
2d: Loop to 2b until no more fields
And my haskell working proto type is this:
module Main where
-- Env User Report Version HostPrinter
egdata1 = [((PD7334EU, *ALL, *ALL,*ALL, *ALL), Default
Printer),
((PD7334EU, USER1, *ALL,*ALL, *ALL),
User1Printer),
((PD7334EU, USER2, Report1, Version1, *ALL),
User1Report1Printer),
((PD7334EU, *ALL, Report2, *ALL, *ALL),
Report2Printer)]
type SearchFilter = (String, String, String, String, String)
type Record = (SearchFilter, String)
findPrinter :: String - String - String - String - String - [Record]
- String
findPrinter env user report version host printerdata =
findPrinter' sf sf printerdata
where
sf = (env, user, report, version, host)
findPrinter' :: SearchFilter - SearchFilter - [Record] - String
findPrinter' (*ALL, *ALL, *ALL, *ALL, *ALL) _ _ =
findPrinter' sf origsf printerdata
| printer === findPrinter' (toggle sf origsf 5) origsf
printerdata
| otherwise = printer
where
printer = searchPrinter sf printerdata
searchPrinter :: SearchFilter - [Record] - String
searchPrinter _ [] =
searchPrinter sf ((x,p):xa)
| sf == x= p
| otherwise = searchPrinter sf xa
toggle :: SearchFilter - SearchFilter - Int - SearchFilter
toggle sf origsf 0 = sf
toggle sf origsf n
| newValue == *ALL = newSF
| otherwise= toggle newSF origsf (n-1)
where
newValue = toggleField (getSFField n sf) (getSFField n origsf)
newSF= setSFField n sf newValue
toggleField :: String - String - String
toggleField *ALL x = x
toggleField _ _ = *ALL
getSFField :: Int - SearchFilter - String
getSFField 1 (x,_,_,_,_) = x
getSFField 2 (_,x,_,_,_) = x
getSFField 3 (_,_,x,_,_) = x
getSFField 4 (_,_,_,x,_) = x
getSFField 5 (_,_,_,_,x) = x
setSFField :: Int - SearchFilter - String - SearchFilter
setSFField 1 (a,b,c,d,e) f = (f,b,c,d,e)
setSFField 2 (a,b,c,d,e) f = (a,f,c,d,e)
setSFField 3 (a,b,c,d,e) f = (a,b,f,d,e)
setSFField 4 (a,b,c,d,e) f = (a,b,c,f,e)
setSFField 5 (a,b,c,d,e) f = (a,b,c,d,f)
main = putStrLn (findPrinter PD7334EU USER2 Report2 Version3
SomeHost egdata1)
Re: [Haskell-cafe] closed classes
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 ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed classes
Malcolm Wallace [EMAIL PROTECTED] writes: 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 ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: exceptions vs. Either
On 06/08/2004, at 6:56 PM, MR K P SCHUPKE wrote: After all, Java basically does exactly what you're asking for with Java's head/tail would be doing runtime checks if they are throwing exceptions, static guarantees mean the program would not be allowed to compile if it broke the static guarantees. As Keith said, Java will check at compile time whether or not you handle the exception. My point is this: it is impossible to check whether the exception is properly handled. If you adjust Haskell's tail function to return (Maybe [a]) instead of just ([a]), you are doing the thing as Java from a pragmatic perspective: you are adding information to the type system that tells the programmer the function may fail. You also suffer the same consequence as Java: you have no idea whether the programmer properly handles the error situation. If I am writing a one-shot, never-use-again script that takes 3 minutes to write, and I _know_ that I'm not going to be feeding the tail function a non-empty list--e.g. because I'm writing a one-shot five-minute script to transform a file from one text format to another, as is the case for lots of Perl programs--then the extra Maybe type just gets in the way. I'll either ignore the Nothing case, or write `case tail foo of ... Nothing - error bleh'. I will go so far to say that such a program can be considered correct: it does exactly what I want it to do, in exactly the circumstances I desire (0 byte files being specifically excluded from the circumstances!). Which is a bad thing! All programmers always have to consider error conditions, if they don't they write buggy code - that's the nature of the beast. I prefer making programmers expicitly face the decisions they are making, rather than have things implicitly handled in a way that hides what is going on from the programmer. It's a question of whether the library designer should impose their will on the library user. As a library designer, do you feel that you are always making the right decision for the library user 100% of the time? I know I never feel like that when I write libraries ... -- % Andre Pang : trust.in.love.to.save ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Partial signatures
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. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type classes... popular for newbies, isn't it?
This class definition is giving me a lot of problems with the successor function: class (Ord st) = MinimaxState st where successors:: st - [(action,st)] terminal:: st - Bool A trivial example would be: instance MinimaxState Int where terminal i = i == 0 successors i = [(1,i+1), (-1,i-1)] However, I get this error in GHC: Could not deduce (Num action) from the context (MinimaxState Int, Ord Int) arising from the literal `1' at AbTest.hs:7 Probable fix: Add (Num action) to the class or instance method `successors' In the first argument of `negate', namely `1' In the list element: (- 1, (- i) - 1) In the definition of `successors': successors i = [(1, i + 1), (- 1, (- i) - 1)] I have the class definition and the instance definition in seperate files. I don't understand where I'm supposed to put the probable fix. I don't want it to be in the class definition, since action should be fairly arbitrary. In fact, no matter what I try, I get errors, for example: instance MinimaxState Int where terminal i = i == 0 successors i = [(action,i+1), (action,i-1)] Cannot unify the type-signature variable `action' with the type `[Char]' Expected type: action Inferred type: [Char] In the list element: (action, i + 1) In the definition of `successors': successors i = [(action, i + 1), (action, (- i) - 1)] Any suggestions? -Arjun ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
