Re: [Haskell] pros and cons of static typing and side effects ?
The previous comments make sense to me. The lots-of-unit-tests aspect of static typing I find really useful, far exceeding any BDSM cost. If I'm engaging in exploratory programming, the type inference combined with the ability to write 'error "armadillo"' in stubs for values I can't be bothered to generate right now really works conveniently for me. Although I agree that lots-of-lists is very handy in early prototyping, I don't feel at all constrained by using homogeneous lists, although very occasionally I may use existential types, and the way I write programmes is exactly to think in advance and then write the code: to do otherwise just wastes my time because then the code doesn't work in some confusing way and I have to do that thinking I postponed to figure out why - or, if it does work, I have to think about it to satisfy myself that appearances aren't deceiving. I'm not quite sure what macros would look like in Haskell, but I've not missed those either. In Lisp I would tend to use them for things that involved changing the values of variables, but that's not really a Haskellish thing to be doing anyway. Mind you, I learned Lisp after learning ML, so to some extent I was thinking in ML when writing in Lisp. Alas, dead-tree versions of "On Lisp" are hard to come by affordably, but I am now trying to learn more about what I might have missed about Lisp. I find monads useful because I find it a helpful debugging aid for functions to be quite clear about what side effects they may want to have. I posted this to Haskell-Cafe instead of the main Haskell list, because I'm rambling a bit. Puzzled Haskell-Cafe readers may like to check http://www.mail-archive.com/haskell@haskell.org/msg17009.html -- Mark
My 2-pence worth on static typing. Static typing to me seems to be a simplified form of design by contract. There are some things about a program that can be proved "true for all time". Types are an example of such a thing. We can use type systems to make assertions about properties that must be true for all time, and then reject programs that break these rules. One of the easyest things to prove about a program is that all values and references are handled correctly - hence you will never see a "segmentation fault" due to bad programming, it is just impossible (of course the run-time-system which is written in C may cause one, but that cannot be due to a bug in your program). Taking one of your points in more detail:The single type property for lists is not a problem due to the presence of algebraic datatypes, for example want a list of strings and ints: data StringOrInt = IsString String | IsInt Int type ListOfStringOrInt = [StringOrInt] You can also have lists of records... Think about it for a bit and you will see there are very few cases where you need to have a list of 'general types'... You can even use existential types to create lists of things with a common interface, where you do not know in advance what types you may need: data XWrap = XWrap (forall a . Show a => a) type ListXWrap = [XWrap] This creates a list where the items can be any type, provided they are a member of the class Show. Also the only functions you can call on the items in the list are the methods of the Show class... Of course you can have multiple type constraints (forall a . (Show a,Num a) => a). This is not the limit of how far we can go with static typing. We can choose any provable property about a program... for example we could ask that the compiler prove that the heap size of the program never exceeds 10M (not possible in any current language - but is an extension of the concept). Other things we can do ... with dependant types we can ask the compiler to prove the correctness of sorting algorithms. If we define an ordered list tgo be one where each element must be larger than the preceding one: data OrderedIntList = Cons (a::Int) (l::OrderedList) | Nil {- where a <= head l -} data IntList = [Int] We can now define our sorting function: quicksort :: IntList -> OrderedIntList By this we are asking the compiler to prove (by induction) that the function provided can only result in correctly ordered lists - irrespective of what arguments it is given (ie proved true for any input)... This would have to be done symbolically but is not beyond what can be achieved using logic programming. To implement this, a Prolog program containing all the type constraints of the function definition and the "proposed" type would be evaluated... Prolog will say "yes" or "no" to the function. Regards, Keean.
On Tuesday 16 August 2005 21:56, Keean Schupke wrote:
You can even use existential types to create lists of things with a common interface, where you do not know in advance what types you may need:
data XWrap = XWrap (forall a . Show a => a) type ListXWrap = [XWrap]
You probably meant to write data XWrap = forall a . Show a => XWrap a or, in GADT style (which I find a bit more intuitive here): data XWrap where XWrap :: Show a => a -> XWrap Ben
Benjamin Franksen wrote:
On Tuesday 16 August 2005 21:56, Keean Schupke wrote:
You can even use existential types to create lists of things with a common interface, where you do not know in advance what types you may need:
data XWrap = XWrap (forall a . Show a => a) type ListXWrap = [XWrap]
You probably meant to write
data XWrap = forall a . Show a => XWrap a
or, in GADT style (which I find a bit more intuitive here):
data XWrap where XWrap :: Show a => a -> XWrap
Yes I always get confused by the notation Haskell uses... I used explicit universal quantification by mistake. I tried to think logically about the encapsulation existential types represent - and got the wrong form. I for one would like to see the use of 'exists' as a keyword for existential types, after all different symbols are used in modal logic (upside-down-A for forall, and backwards-E for exists). Regards, Keean.
On Tuesday 16 August 2005 22:29, Keean Schupke wrote:
Benjamin Franksen wrote:
On Tuesday 16 August 2005 21:56, Keean Schupke wrote:
You can even use existential types to create lists of things with a common interface, where you do not know in advance what types you may need:
data XWrap = XWrap (forall a . Show a => a) type ListXWrap = [XWrap]
You probably meant to write
data XWrap = forall a . Show a => XWrap a
or, in GADT style (which I find a bit more intuitive here):
data XWrap where XWrap :: Show a => a -> XWrap
Yes I always get confused by the notation Haskell uses...
Same here.
I used explicit universal quantification by mistake. I tried to think logically about the encapsulation existential types represent - and got the wrong form.
I for one would like to see the use of 'exists' as a keyword for existential types, after all different symbols are used in modal logic (upside-down-A for forall, and backwards-E for exists).
I once read a paper about type classes and existentials (can't remember exact title or author, was it Läufer?) where the proposal was to make existential quantification implicit (just as the universal one is in Haskell98). That is, any type variable that appears on the rhs of a data type, but not on the lhs, is implicitly existentially quantified, as in data XWrap = Show a => XWrap a I always thought this was a pretty nice idea. Ben
Benjamin Franksen wrote:
as in
data XWrap = Show a => XWrap a
I always thought this was a pretty nice idea.
Wow, I hadn't thought of that... of course you still need to explicitly give the universal quantification if you need it. I guess the best option is to make it optional, as I still like the look of: data XWrap = exists a . Show a => XWrap a It kind of say "this is existential quantification" in large freindly letters... (A bit like a book I once read - except that said "Don't Panic") Keean.
Keean Schupke wrote:
Other things we can do ... with dependant types we can ask the compiler to prove the correctness of sorting algorithms. If we define an ordered list tgo be one where each element must be larger than the preceding one:
data OrderedIntList = Cons (a::Int) (l::OrderedList) | Nil {- where a <= head l -} data IntList = [Int]
We can now define our sorting function:
quicksort :: IntList -> OrderedIntList
By this we are asking the compiler to prove (by induction) that the function provided can only result in correctly ordered lists - irrespective of what arguments it is given (ie proved true for any input)... This would have to be done symbolically but is not beyond what can be achieved using logic programming.
But the output being ordered is not enough. The output should also be a permutation of the input. This can, of course, be expressed in a similar way. -- Lennart
Lennart Augustsson wrote:
Keean Schupke wrote:
quicksort :: IntList -> OrderedIntList
By this we are asking the compiler to prove (by induction) that the function provided can only result in correctly ordered lists - irrespective of what arguments it is given (ie proved true for any input)... This would have to be done symbolically but is not beyond what can be achieved using logic programming.
But the output being ordered is not enough. The output should also be a permutation of the input. This can, of course, be expressed in a similar way.
Yes, the easiest way would be to constrain the output list to be a subset of the input list, and vice-versa... something like: quicksort :: (x::IntList) -> (y::OrderedIntList) {- where x :< y && x :> y -} of course you would have to use the correct definition of subset - you really want to treat the list as a multi-set. Keean.
participants (4)
-
Benjamin Franksen -
Keean Schupke -
Lennart Augustsson -
Mark Carroll