Version française
Home     About     Download     Resources     Contact us    
Browse thread
Stdlib regularity
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Jean-Francois Monin <JeanFrancois.Monin@c...>
Subject: Re: Proposal for study: Add a categorical Initial type to ocaml
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