**Next message:**Damien Doligez: "Re: speed versus C"**Previous message:**Jacques Garrigue: "Option types and O'Labl merger"**Next in thread:**Damien Doligez: "Re: Proposal for study: Add a categorical Initial type to ocaml"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

Date: Tue, 12 Oct 1999 13:33:25 +0200

Message-Id: <199910121133.NAA27629@lsun565.lannion.cnet.fr>

From: Jean-Francois Monin <JeanFrancois.Monin@cnet.francetelecom.fr>

To: skaller <skaller@maxtal.com.au>

Subject: Re: Proposal for study: Add a categorical Initial type to ocaml

In-Reply-To: <38002EBF.DF0EF779@maxtal.com.au>

<37FC6572.719AD12D@tsc.uc3m.es>

I'm not sure that category theory helps so much here.

My own background in cat. th. is weak, here is my understanding:

- unit is final because there is one & only one function from any type

to unit, namely fun _ -> ()

- an initial type, say ini, is a type s.t. we have one & only one function

from ini to any type;

this should be the empty sum with no contructor:

type emp = ;;

The initial function would be

let ini (x: emp) = match x with ;;

Note that this is syntactically not allowed in ocaml. I don't think

there is a theoretical problem to add it (at least there are

extensions of caml type system allowing this) , however such a type would be

intrinsically useless (without real use). In particular your '$' seems

inconsistent to me. The only way to "get" such a value is to

introduce it locally in the context, e.g. fun x -> x, or in your case

let f dollar = let x = { data = ini dollar }

which will never help !

[John Prevost <prevost@maya.com> wrote:]

*> I would like to propose adding a new special type to ocaml,
*

*> a categorical initial type. This type is the categorical dual
*

*> of the categorical terminal type, unit.
*

*>
*

*> There proposal is for a syntactic designator (say '$') for the
*

*> non-existant value of the initial type, which can
*

*> be bound to a variable of any type.
*

*> [You could say it has type 'a, as does 'raise SomeException']
*

*>
*

*> The effect of attempting to read this value from any type
*

*> should be to raise the exception Uninitialised_value.
*

*>
*

*> Example:
*

*>
*

*> type A = { data: t }
*

*> let x = { data = $ }
*

*> in x.data (* raises exception *)
*

Jean-Francois Monin

**Next message:**Damien Doligez: "Re: speed versus C"**Previous message:**Jacques Garrigue: "Option types and O'Labl merger"**Next in thread:**Damien Doligez: "Re: Proposal for study: Add a categorical Initial type to ocaml"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

*
This archive was generated by hypermail 2b29
: Sun Jan 02 2000 - 11:58:27 MET
*