Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: donald.syme@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu
In-Reply-To: <"swan.cl.cam.:138520:950425190942"@cl.cam.ac.uk> (message from Donald Syme on Tue, 25 Apr 1995 21:09:27 +0200)
Subject: Re: A trivial "option" library
Message-Id: <95Apr26.004705met_dst.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 26 Apr 1995 00:47:00 +0200


Don writes

> I've been thinking that a (trivial) "option" library should be included
> with HOL.  This would just be the type
> 
> 	option = SOME of 'a | NONE
>
> I think the only constants besides SOME and NONE I will include will
> be IS_SOME and IS_NONE.

I agree that the "option" type should be defined early on in the
development of the logic. However, be warned that functional programmers
will shout in unison: "It's a Monad!". You might want to include a
composition operator to mollify them. With a "case" definition

    (option_case u f NONE = u)
    (option_case u f (SOME x) = f x)

monad "composition" is easy to define and its rewrite rules are trivial
consequences:

    comp f =def= option_case NONE (SOME o f)

    comp f NONE = NONE
    comp f (SOME x) = SOME (f x)

Of course "comp" could be directly defined, but case theorems are
generally useful, as they largely remove the need for discrimination and
destruction functions for examining values of datatypes. As such, they
are a natural way to represent pattern matching lambda terms (and case
expressions, of course). For example, the following (inventing some
syntax):

       \NONE. foo 
    || \SOME x. bar[x]

could be represented by the term

    option_case foo (\x. b[x])


Konrad.