A Pointless Library Proposal
Conor McBride
ctm at Cs.Nott.AC.UK
Mon Oct 23 17:43:36 EDT 2006
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.
More information about the Libraries
mailing list