[isabelle-dev] HOLCF lists

[Brian Huffman]

On Wed, Jul 18, 2012 at 8:52 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> On 07/17/2012 07:53 PM, Brian Huffman wrote:
>> HOLCF/Library/{Nat,Int}_Discrete.thy define cpo instances for types
>> nat and int, so you can write types like "nat -> 'a list" or
>> "nat\<^sub>\<bottom> -> 'a list". Decisions about which types to use
>> should probably follow Haskell: "Integer" should be modeled as
>> "int\<^sub>\<bottom>" or "int lift", and for unboxed Haskell types
>> (e.g. Int#) you can use "int".
>
> Sorry for asking stupid questions (since I am to lazy to look it up myself):
> what's the difference between "'a lift" and "'a u" exactly? Is either of
> them preferable to model "Haskell-Integers"? I tried to instantiate "'a u"
> for my eq-class, but failed due to sort problems, since I'm not that
> familiar with the type class hierarchy of HOLCF, maybe you could save me
> some time ;).

Type "'a u" or "'a\<^sub>\<bottom>" requires its argument to have
class "cpo". The ordering on "'a u" is the same as 'a, but with a new
bottom element.

Type 'a lift only requires its argument to have class "type"; the
ordering is always a flat pcpo. It is intended for use with HOL types
without cpo instances.

If 'a is a cpo with a discrete ordering, then 'a u and 'a lift are
isomorphic. However, I consider it a bad practice to use "lift" with
any type that actually has a cpo instance.

For modeling Haskell integers, I would suggest using "nat lift", "int
lift", etc. if you are not using the {Nat,Int}_Discrete libraries, but
if you are, I would prefer using "nat u" or "int u".

> Btw: any more thoughts on actually putting code into some publicly available
> destination (bitbucket, sourceforge, ...)?

If you want to set up a bitbucket or sourceforge repo for this
purpose, that would be great. I'd be happy to contribute to something
like that.

- Brian