Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
From: Goswin von Brederlow <goswin-v-b@web.de>
To: bluestorm <bluestorm.dylc@gmail.com>
Cc: Lukasz Stafiniak <lukstafi@gmail.com>, caml-list@inria.fr
Subject: Re: [Caml-list] Conditionals based on phantom types
Date: Tue, 03 Aug 2010 17:47:12 +0200	[thread overview]
Message-ID: <87r5if4s1r.fsf@frosties.localdomain> (raw)
In-Reply-To: <AANLkTi=55+Wu+dKEB8Tt6bwkmxzSRB_JKsnGhUOFDdiK@mail.gmail.com> (bluestorm's message of "Mon, 2 Aug 2010 10:02:41 +0200")

bluestorm <bluestorm.dylc@gmail.com> writes:

> Two remarks on Lukasz suggestion :
>
>>   val add : 'a t -> 'a t -> 'a t
>>   [..]
>>   let add (_,x) (_,y) = x +. y
>
> This does not typecheck. I suggest the following :
>
> let add (ux, x) (uy, y) =
>   assert (ux = uy);
>   (ux, x +. y)
>
> While the assertion does not seem necessary at first (correct units
> are guaranteed by typing !), it may be helpful in case of bug inside
> the Units module or signature, wich breaks the typing invariant. If
> you're planning to do relatively elaborate things inside the Units, I
> strongly recommend to use any kind of dynamic checking available, at
> least during development. This is something is understood late in my
> own phantom-type project (Macaque), and would have been very useful
> for debugging.

I tend to hide the phantom tpyes in a submodule with just the bare
minimum of function (creation and access) included and then use the
submodule in the actual module. That way the phantom types are verified
in the actual module too. Instead of assertion failures at runtie you
get compiler errors.

MfG
        Goswin


  parent reply	other threads:[~2010-08-03 15:47 UTC|newest]

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2010-08-02  7:07 Joseph Young
2010-08-02  7:49 ` [Caml-list] " Lukasz Stafiniak
2010-08-02  8:02   ` bluestorm
2010-08-03  2:46     ` Joseph Young
2010-08-03  6:15       ` Joseph Young
2010-08-03  6:57         ` bluestorm
2010-08-04  2:41           ` Joseph Young
2010-08-03 15:47     ` Goswin von Brederlow [this message]
2010-08-03 15:39 ` Goswin von Brederlow

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=87r5if4s1r.fsf@frosties.localdomain \
    --to=goswin-v-b@web.de \
    --cc=bluestorm.dylc@gmail.com \
    --cc=caml-list@inria.fr \
    --cc=lukstafi@gmail.com \
    /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