Stdlib regularity
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  JeanFrancois 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 > nonexistant 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 *) JeanFrancois Monin