[Haskell-cafe] Optimization with Strings ?

[Jason Dagit]

On Thu, Dec 3, 2009 at 8:25 AM, John D. Earle <JohnDEarle at cox.net> wrote:

> Haskell has a problem with its type system and is not rigorous. Haskell is
> not a suitable language for proof assistants and so I would advise you to
> stay clear of Haskell. Standard ML was engineered with the needs of proof
> assistants in mind and so you may want to look into Standard ML, but you
> should be very happy with Objective CAML. It has an excellent reputation.
> The Coq proof assistant which is another French product is based on
> Objective CAML.
>

If I understand you correctly, SML was engineered with the needs of a proof
assistant in mind, but OCaml is a very different language.  And it seems you
are pushing F#/OCaml not SML.  Do F# and OCaml have full formal semantics
for their type systems that have been verified?  Or are they "merely" based
on Hindley-Milner type systems?  If it is the latter, then could you help me
understand why Haskell is so much worse?  If it's the former could you
please point me to the appropriate research so I can educate myself? If the
objection is primarily String performance based then I would recommend that
you take a look at ByteString or uvector.

Please help me understand the holes in Haskell's type system.  Have you
published some research on the flaws of Haskell's design?  If Haskell is
unsound I'd certainly like to know where and why so that I can improve my
programs.  Please help.

Thanks,
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20091204/cf7d49cf/attachment.html