caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
To: daniel.buenzli@epfl.ch
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods
Date: Wed, 28 Feb 2007 13:01:15 +0900 (JST)	[thread overview]
Message-ID: <20070228.130115.35466734.garrigue@math.nagoya-u.ac.jp> (raw)
In-Reply-To: <8DF1B76F-AE3B-43F2-9034-7CF47277EE7B@epfl.ch>

From: Daniel Bünzli <daniel.buenzli@epfl.ch>
> Le 28 févr. 07 à 02:57, skaller a écrit :
> 
> > After all a nominal type is just a structural type with
> > a unique tag representing its unique name.
> 
> What you miss here is the _process_ behind nominal types.
> 
> (paraphrasing Jacques) Types are not precise enough to define the  
> semantic of a function, multiplication and addition have the same  
> type but in many cases you cannot exchange one for the other. With  
> that respect structural typing is a fallacy, it is not because types  
> match that you can replace a function by another.
> 
> With a nominal type the programmer signals explicitely its intent to  
> support a semantic. Notably you cannot use a function in a given  
> context if it was not designed for that purpose which sounds  
> fascistic but makes sense from a software development point of view.
> 
> Structural typing would make sense if it involved the weakest  
> invariants a function. But for now, because of the poor information  
> types give about semantics, structural typing is just bureaucratic  
> compliance whereas nominal typing is a semantic contract --- whether  
> actually fulfilled or not is another (undecidable) question.

Wow, here is a strong statement. Basically, you seem to be saying that
types are useless for safety if they don't ensure full correctness,
and that in the absence of safety they need to be nominal in order to
declare any intent?

I personally would contradict you on both counts.

The first point is that type safety is already an important form of
safety. Even if it is purely bureaucratic, at least it ensures that
there is no contradiction _at the level of types_. If you are an ML
programmer, you must know that this is useful.

The second point is on the extra semantic advantage of using nominal
types. I think there is some mixing up here. You can perfectly put a
name on a value without using a nominal type. Using good function
names, labelled arguments, etc... And writing (`Metre 3) gives you
exactly the same information as (Metre 3). By naming things, even
structurally, you can express informal contracts.

The theoretical problem with structural types is more about very bad
luck: you may be using two libraries, which seem to be using the same
type (same constructor or method names), but actually have different
semantics.  And you might end up mixing data from the two libraries by
error. The probability of this happening is so incredibly low that I
often wonder why people see this as a real problem, but this reflects
the lack of proper identity in structural types. This lack of identity
may become a problem when you want to use identity for other things,
like privacy. But it is not really relevant for normal public types,
since you may easily deconstruct and reconstruct them. On the other
hand, if you (rightly) decide to use abstract types in an API, whether
they are internally nominal or structural is not relevant.

If I may add a 3rd point, I believe that structural types sometimes
allow you to give more precise specifications of functions, that would
be hard to obtain with nominal types. See the use of polymorphic
variants in lablGL for instance. This is certainly not a complete
specification, all the less as the API is imperative. But this
information can work as documentation, and removes an important
category of runtime errors.

Jacques Garrigue


  reply	other threads:[~2007-02-28  4:01 UTC|newest]

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <301730110702251747y72ae9fbdqd33bd8d08293cbe3@mail.gmail.com>
2007-02-27 21:22 ` Geoffrey Romer
2007-02-28  0:23   ` [Caml-list] " Jacques Garrigue
2007-02-28  1:18     ` Lukasz Stafiniak
2007-02-28  1:34       ` Jacques Garrigue
2007-02-28  1:57         ` skaller
2007-02-28  3:23           ` Daniel Bünzli
2007-02-28  4:01             ` Jacques Garrigue [this message]
2007-02-28  5:09               ` skaller
2007-02-28 13:47               ` Daniel Bünzli

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20070228.130115.35466734.garrigue@math.nagoya-u.ac.jp \
    --to=garrigue@math.nagoya-u.ac.jp \
    --cc=caml-list@inria.fr \
    --cc=daniel.buenzli@epfl.ch \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).