On Thu, Dec 3, 2009 at 8:25 AM, John D. Earle <JohnDEarle@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