From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,c406e0c4a6eb74ed X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news2.google.com!news.maxwell.syr.edu!newsfeed.icl.net!news.tele.dk!news.tele.dk!small.news.tele.dk!news-FFM2.ecrc.net!rcn!feed3.news.rcn.net!not-for-mail From: jayessay Newsgroups: comp.lang.ada Subject: Re: Formal and informal type systems? Date: 28 Sep 2004 16:19:08 -0400 Organization: Tangible Sender: jsa@rigel.goldenthreadtech.com Message-ID: References: <49dc98cf.0408110556.18ae7df@posting.google.com> <413e2fbd$0$30586$626a14ce@news.free.fr> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: UmFuZG9tSVaN6/SkAqryWMV1DbdmaK8QmJDTVlBIfywkOym9R/LISg4mOJ+3Pf22 X-Complaints-To: abuse@rcn.com NNTP-Posting-Date: 28 Sep 2004 20:12:22 GMT User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 Xref: g2news1.google.com comp.lang.ada:4336 Date: 2004-09-28T20:12:22+00:00 List-Id: Mark Lorenzen writes: > Jacob Sparre Andersen writes: > > > Jayessay wrote: > > > > > [Aside: I believe that formal type systems like those of Haskell, > > > OCAML, et.al. are much more potent than the informal ones of Ada, > > > C++, Java, etc. > > > > In what way is the OCAML (I don't know Haskell) type system formal in > > contrast to that of Ada? In what way do you consider it more potent. > > And is that good? (I don't consider C++ templates better than Ada > > generics even though I agree that they are more potent - in dangerous > > ways.) > Google for Hindley-Milner to get papers which cover this in detail. The system is formal in the sense of "mathematically formal". It is more potent as it supports type inference and can be formally reasoned about. It is good to the extent that it directly supports automated proofs of programs (indeed, FP folks will claim that due to this, only "correct" programs are possible, but the notion is oddly idiosynchratic and borders on circularity). > Some things I miss in Ada that are available in ML: Higher order > functions, pattern matching and tuples. That has nothing to do with the type system. Lisp (obviously) also has higher order functions, Common Lisp has argument pattern matching via generic functions (especially via the eql specializer), etc. /Jon -- 'j' - a n t h o n y at romeo/charley/november com