From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: weis
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id QAA00137 for caml-redistribution; Tue, 12 Oct 1999 16:21:41 +0200 (MET DST)
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id NAA04398 for <caml-list@pauillac.inria.fr>; Tue, 12 Oct 1999 13:33:29 +0200 (MET DST)
Received: from p-voyageur.issy.cnet.fr (p-voyageur.issy.cnet.fr [139.100.0.39])
	by nez-perce.inria.fr (8.8.7/8.8.7) with SMTP id NAA17607
	for <caml-list@inria.fr>; Tue, 12 Oct 1999 13:33:28 +0200 (MET DST)
Received: from l-mhs1.lannion.cnet.fr ([161.104.1.59]) by p-voyageur.issy.cnet.fr with SMTP (Microsoft Exchange Internet Mail Service Version 5.5.2448.0)
	id 4Q2WM18Y; Tue, 12 Oct 1999 13:33:12 +0200
Received: from lsun169.cnet (lsun169.lannion.cnet.fr [161.104.4.4]) by l-mhs1.lannion.cnet.fr with SMTP (Microsoft Exchange Internet Mail Service Version 5.5.2448.0)
	id TT0PAPS7; Tue, 12 Oct 1999 13:35:36 +0200
Received: from lsun565.lannion.cnet.fr (lsun565 [161.104.10.182])
	by lsun169.cnet (8.8.8+Sun/8.8.8) with SMTP id NAA01615;
	Tue, 12 Oct 1999 13:33:26 +0200 (MET DST)
Received: from lsun565.cnet by lsun565.lannion.cnet.fr (SMI-8.6/SMI-SVR4)
	id NAA27629; Tue, 12 Oct 1999 13:33:25 +0200
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>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
To: skaller <skaller@maxtal.com.au>
Cc: John Prevost <prevost@maya.com>, caml-list@inria.fr
Subject: Re: Proposal for study: Add a categorical Initial type to ocaml
In-Reply-To: <38002EBF.DF0EF779@maxtal.com.au>
References: <Pine.LNX.4.10.9910060925320.18180-100000@mojave.cs.cornell.edu>
	<37FC6572.719AD12D@tsc.uc3m.es>
	<37FE1E1F.4790FE85@maxtal.com.au>
	<ya2n1tsb1ew.fsf@po.maya.com>
	<38002EBF.DF0EF779@maxtal.com.au>
X-Mailer: VM 6.37 under Emacs 20.2.1
Sender: weis

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