A Pointless Library Proposal

[Conor McBride]

Hi

John Meacham wrote:
> On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
>   
>> This seems like the ideal time to make a wannabe library proposal which
>> is pointless, but pointless by design. The code's quite short:
>>     
>
> so, just to clarify, is what you are proposing is a type whose only
> inhabitant is _|_, and since _|_ inhabits all types, we should be able
> to freely cast this bottom-only-containing type to any other?
>   

Exactly, although I prefer to avoid talking about _|_ unless I
absolutely have to. The fact that there are no values worth speaking of
in |Zero| is a good way of pinning down the /absence/ of things, hence
the use of |Tm Zero| to represent terms with no free variables.
Moreover, general tree-like structures given by fixpoints of functors

> data Fix f = In (f (Fix f))

have a general notion of |leaf|

> leaf :: Functor f => f Zero -> Fix f
> leaf = In . fMagic

If you're interested in calculating types of one-hole contexts, then
|Zero| is very handy

> class (Functor f, Functor g) => Diff f g | f -> g where ...

> instance Diff (Const c) (Const Zero) where ...
> instance Diff Id (Const ()) where ...
> instance (Diff f f', Diff g g') => Diff (Sum f g) (Sum f' g') where ...
> instance (Diff f f', Diff g g') => Diff (Prod f g) (Sum (Prod f' g) 
(Prod f g')) where ...

where Sum and Prod are Either and (,) lifted pointwise to kind * -> *

> Sounds good to me. I can't think of a use off the top of my head, but I
> ended up using Identity all over the place... and this sounds like just
> the random sort of thing I will find odd uses for. :)
>   

so plenty of odd uses!

> but since 'Zero' is often used in type arithmetic implementations (even
> though those uses arn't entirely incompatable) I think we should name it
> something else.

I think the two go very well together. If you define

> data Suc n = New | Old n

then the type-level unary numbers double as types with that many values
worth speaking of. I'm rather fond of the idea that |Tm (Suc (Suc
Zero))| is the type of terms in two free variables, and so on. You also
get that addition, multiplication, etc, for type-level numbers
correspond to, er, sum, product, etc for the types.

I know this kind of breaks the singleton hack to give run-time proxies
for static types, but there are other ways to make proxies.

>  I think
>
> data Bottom 
>
> is waht I would like.
>   

This is one thing we've got that we shouldn't flaunt. If I can't have
Zero, please may I have

> data Naught

> naughty :: Naught -> y

> innocent :: Functor f => f Naught -> f x

or some such?

Cheers

Conor



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.