Version française
Home     About     Download     Resources     Contact us    
Browse thread
Re: Proposal for study: Add a categorical Initial type to ocaml
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: chet@w...
Subject: Re: Proposal for study: Add a categorical Initial type to ocaml

Of course, it is problematic that "None" and "Some None" are
indistinguishable.  But is it a reason to not have such a facility (as
a storage-cost-free "option" type constructor)?

I'd like to believe that the answer is "no" -- that the efficiency
values of such a type-constructor outweigh the semantic difficulties.

Of course, there's only one way to prove that -- by implementing both
and trying it out on large programs.

--chet--

>>>>> "WC" == William Chesters <williamc@dai.ed.ac.uk> writes:

    WC> The problem is that if you have a value of the type `int
    WC> option option', you have to be able to distinguish between
    WC> `None' and `Some None'!  If both the enumeration-indirections
    WC> are elided, you can't; if only one of them is, you have
    WC> inconsistency which would presumably have to be resolved using
    WC> whole-program optimisation or something.