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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,24d7acf9b853aac8 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!cleanfeed4-a.proxad.net!nnrp20-2.free.fr!not-for-mail Date: Wed, 11 Aug 2010 01:04:29 +0200 From: _FrnchFrgg_ User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.10) Gecko/20100619 Icedove/3.0.5 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: S-expression I/O in Ada References: <547afa6b-731e-475f-a7f2-eaefefb25861@k8g2000prh.googlegroups.com> <46866b8yq8nn$.151lqiwa0y2k6.dlg@40tude.net> <13b07f2c-2f35-43e0-83c5-1b572c65d323@y11g2000yqm.googlegroups.com> <13tpf7ya3evig$.h05p3x08059s$.dlg@40tude.net> <1omt2srxtpsga$.c3hbxthzo6cf.dlg@40tude.net> <1e4cch2df5uyb.18brqdd16dhv8.dlg@40tude.net> <14y70ke8am9qw$.2csc9eflvigg.dlg@40tude.net> <4c601b5c$0$7665$9b4e6d93@newsspool1.arcor-online.net> <9czktq4ntzq7.fhbsnocx0x4w$.dlg@40tude.net> <4c6078f9$0$12500$426a74cc@news.free.fr> <4c6132d2$0$8378$426a74cc@news.free.fr> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Message-ID: <4c61dafd$0$14549$426a74cc@news.free.fr> Organization: Guest of ProXad - France NNTP-Posting-Date: 11 Aug 2010 01:04:29 MEST NNTP-Posting-Host: 82.233.38.63 X-Trace: 1281481469 news-3.free.fr 14549 82.233.38.63:38288 X-Complaints-To: abuse@proxad.net Xref: g2news1.google.com comp.lang.ada:13096 Date: 2010-08-11T01:04:29+02:00 List-Id: Le 10/08/2010 13:19, Dmitry A. Kazakov a �crit : > On Tue, 10 Aug 2010 13:06:58 +0200, _FrnchFrgg_ wrote: >> Unification and pattern matching is independent of type inference. > > Did you mean the standard meaning of pattern matching instead of Standard > ML's Volap�k? I meant pattern matching as a ML construct, which is in fact structural unification. It can be done even without type inference, and only needs some kind of polymorphism; essentially you have an object and an expression made of (possibly nested) constructors, with leaves being either constants or variables, and the unification engine answers a) if the object could be obtained by the sequence of constructors, or not b) if yes, the content the variables would have had so that the sequence of constructors would produce the object. For convenience, you often have a list of expressions, and the engine executes the code of the first which fits the object. Of course, if you don't want a type orgy (aka dynamic types), you'd probably want all the constructor expressions create subtypes of a base one, and the object also be a subtype of this base one. When the language also does type inference, then this "greatest common denominator" is calculated at compile-time (and the language typically is able to tell you have forgotten to cover all possible constructor sequences for the type). But nothing prevents a language to require explicit types and enforce them just by checking with no inference at all. And in fact, IIRC I was shown a language having unification without type inference (not PROLOG, because its unification is for predicates and doesn't count). I do not recall the name of the language (it was probably not much used). Anyway OCaml could arguably be considered as an exemple(1). Note that "pattern matching" as described here is well tailored to immutable objects; I think there are ways to accomodate mutability, but I do not remember clearly. Since OCaml has mutability in objects if wanted, and pattern matching on objects (not only on algebraic types), I suppose they solved the problem in some way. (1) Even if you don't like type inference (and I agree that a human reading the code shouldn't be required to "infer" the types, and as such that types should be annotated), every language I know with type inference accepts explicit type annotations so you can always type explicitly every variable and you exactly get a strongly, explicitely typed language.