Re: [Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
Martin Vlk [EMAIL PROTECTED] writes: http://www-i2.informatik.rwth-aachen.de/Staff/Current/michaelw/sttt-ml-haskell.pdf Interesting to see others' experiences, even if they are slightly negative. It contains descriptions of lots of real-world problems and how They are only implementing TRUTH and CWB, no? Among other things it touches on the static typing pros and cons One critique against the paper is that they discuss language features at great length, but conclude that: |However, it turned out in our discussions that none of us were | enthusiastic about the idea of using a functional language for a | future verification tool because of their impoverished environments | compared with mainstream programming languages. I would like to see more discussion of what is impoverished about the environments, and what they consider mainstream programming languages. Certainly the authors could have discussed this in the main part of the paper? | Our impression was that SML and Haskell can play out their | advantages mainly in the prototyping stages of a project, an arena | where both would have to compete with dynamic languages like Lisp or | Smalltalk, or scripting languages like Python (which have faster | turn-aroundcycles due to absence of a compilation phase). I'm not sure the authors are even aware or the existence of interactive environments (e.g. Hugs and GHCi are not mentioned, only Haskell *compilers*). Disclaimer: I just browsed quickly through the paper. -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
Hi folks, have you read this paper: http://www-i2.informatik.rwth-aachen.de/Staff/Current/michaelw/sttt-ml-haskell.pdf It contains descriptions of lots of real-world problems and how easily they are solved with Haskell (and ML, because the paper compares the two languages). Among other things it touches on the static typing pros and cons in a way that anyone who ever did serious programming will understand. vlcak ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?
[Moved to the Haskell cafe] It's Friday afternoon here so I thought I'd join in the fun. On Thu, 2005-08-11 at 23:01 -0400, [EMAIL PROTECTED] wrote: While you can't be certain that once your code typechecks, it's bug-free (though that does often happen), you can be almost guaranteed that if your code typechecks after a refactoring, the refactoring didn't introduce any bugs. (I tend to agree with ajb's sentiment, but I'll play the devil's advocate anyway). Perhaps we can reach a fixed point of violent agreement? I'm a bit concerned with can't be certain on the one hand, and _almost_ guaranteed, on the other. I guess there are nuances to be explored here, and it is all about degree of confidence. Sometimes I have high confidence in my refactoring, like introducing a state monad. Other times I have much less confidence, like swapping the order of arguments in numerical calculations. However, if it weren't for static type checking then I would be much less game to even _try_ introducing a state monad in my code in the first place. (Maybe that's just me). Another colleague of mine gave the opinion that one of the reasons higher-order code is less common in Prolog than Haskell is that in Prolog does not have static type checking (it's just one factor out of many). It seems to me like static type checking has the capacity to make some refactorings much less heroic than they would be in the non-static setting. That's my log on the fire for today. Bernie. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
