<br><br><div class="gmail_quote">On Thu, Dec 3, 2009 at 8:25 AM, John D. Earle <span dir="ltr"><<a href="mailto:JohnDEarle@cox.net">JohnDEarle@cox.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div style="padding-left: 10px; padding-right: 10px; padding-top: 15px;" name="Compose message area"><div><font face="LM Mono 12" size="4">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.</font></div></div></blockquote><div><br>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. <br>
<br>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.<br>
<br>Thanks,<br>Jason<br></div></div>