A Pointless Library Proposal

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
44 messages Options
123
Reply | Threaded
Open this post in threaded view
|

A Pointless Library Proposal

Conor McBride
Hi folks

This seems like the ideal time to make a wannabe library proposal which
is pointless, but pointless by design. The code's quite short:

----------

> module Zero where

> -- import GHC.Prim -- if you can

The Zero type has nothing in it. Well, nothing worth worrying about anyway.

> data Zero

Elements of Zero are rather special, powerful things.

> magic :: Zero -> a
> magic _ = error "There's magic, as no such thing!"

It's a little frustrating to have to define this function lazily. I
prefer the strict definition with no lines, but it isn't valid
Haskell!

The main use of Zero is to give types |f Zero| to the closed
('elementless') values of some functorial structure f, especially
closed /terms/. These closed values should be embedded (as cheaply as
possible) into all the f-types which do permit elements.

> fMagic :: Functor f => f Zero -> f a
> fMagic = fmap magic -- if you must
> -- fMagic = unsafeCoerce# -- if you can

-----------

I'm not being facetious here. The reason it ought to be in a library
rather than ad hoc is that it (ideally) packs up a perfectly safe use of
unsafeCoerce#, which deserves some veneer of legitimacy. This is
seriously useful stuff if you want better static checking for scope (and
related notions), without taking a performace hit.

For example, you should all know the classic de Bruijn representation...

> data Tm x = V x | A (Tm x) (Tm x) | L (Tm (Maybe x)) deriving Show

...for which fmap does renaming...

> instance Functor Tm where
>   fmap rho (V x)   = V (rho x)
>   fmap rho (A f a) = A (fmap rho f) (fmap rho a)
>   fmap rho (L b)   = L (fmap (fmap rho) b)

...and (>>=) does capture-avoiding simultaneous substitution.

> instance Monad Tm where
>   return = V
>   V x   >>= sgm = sgm x
>   A f a >>= sgm = A (f >>= sgm) (a >>= sgm)
>   L b   >>= sgm = L (b >>= shift sgm) where
>     shift sgm Nothing  = V Nothing
>     shift sgm (Just x) = fmap Just (sgm x)

But operationally, you'd never do any such thing. See how capture is
avoided? The shift operator (aka traverse, but that's another story),
has to tweak all the free variables in the image of the substitution to
avoid capturing the new bound variable, Nothing. Ouch!

However, if you've ever fooled around with Int-based de Bruijn
representations, you'll know that the really cool thing is to substitute
/closed/ terms without any need for shifting. A term with no free
variables can't capture anything! Hence

> closedSubst :: (x -> Either (Tm Zero) y) -> Tm x -> Tm y
> closedSubst sgm (V x)    = either fMagic V (sgm x)
> closedSubst sgm (A f a)  = A (closedSubst sgm f) (closedSubst sgm a)
> closedSubst sgm (L b)    = L (closedSubst (shift sgm) b) where
>   shift sgm Nothing  = Right Nothing
>   shift sgm (Just x) = either Left (Right . Just) (sgm x)

Here, variables are either mapped to closed terms or renamed. We never
need to traverse the closed terms to push them under a binder: the shift
operator (aaka traverse, ahem) only shifts the renaming part (cheap!)
and the closed terms stay closed. When we finally hit a variable, the
closed images just get fMagic'd into the right scope!

So there you have it, a bone fide useful use of the Zero type, given a
module exporting a safe use of a usually dodgy operator. I don't think
module Zero is as pointless as the the datatype it defines.

My apologies for not providing any QuickCheck properties.

All the best

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.

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

John Meacham
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?

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. :)

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

data Bottom

is waht I would like.

        John

--
John Meacham - ⑆repetae.net⑆john⑈
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Samuel Bronson
On 10/23/06, John Meacham <[hidden email]> wrote:
> On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:

> data Bottom
Why not "data Void"?
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Jason Dagit-2
On 10/23/06, Samuel Bronson <[hidden email]> wrote:
> On 10/23/06, John Meacham <[hidden email]> wrote:
> > On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
>
> > data Bottom
> Why not "data Void"?

I'm partial to:
data Intercalate

Jason
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Bugzilla from robdockins@fastmail.fm
On Monday 23 October 2006 17:26, Jason Dagit wrote:

> On 10/23/06, Samuel Bronson <[hidden email]> wrote:
> > On 10/23/06, John Meacham <[hidden email]> wrote:
> > > On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
> > >
> > > data Bottom
> >
> > Why not "data Void"?
>
> I'm partial to:
> data Intercalate

I'd have to vode for:
data BikeShed

Seriously, though.  I prefer 'Void' to 'Bottom'.

> Jason

--
Rob Dockins

Talk softly and drive a Sherman tank.
Laugh hard, it's a long way to the bank.
       -- TMBG
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

John Meacham
In reply to this post by Samuel Bronson
On Mon, Oct 23, 2006 at 05:17:49PM -0400, Samuel Bronson wrote:
> On 10/23/06, John Meacham <[hidden email]> wrote:
> >On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
>
> >data Bottom
> Why not "data Void"?

also good.

or

data Absurd

also works for me.

        John

--
John Meacham - ⑆repetae.net⑆john⑈
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Conor McBride
In reply to this post by John Meacham
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.

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Ashley Yakeley
In reply to this post by Conor McBride
Conor McBride wrote:

>> magic :: Zero -> a
>> magic _ = error "There's magic, as no such thing!"
>
> It's a little frustrating to have to define this function lazily. I
> prefer the strict definition with no lines, but it isn't valid
> Haskell!

This issue comes up a lot with GADTs. For instance:

   data MyGADT a where
     MyInt :: MyGADT Int
     MyChar :: MyGADT Char

   never :: MyGADT Bool -> a

Annoyingly, this doesn't compile without adding a definition line
mentioning a bottom value.

--
Ashley Yakeley

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

John Meacham
In reply to this post by Conor McBride
On Mon, Oct 23, 2006 at 10:43:36PM +0100, Conor McBride wrote:

> 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?

I am liking the 'Void' idea proposed earlier, so we have

> module Data.Void where
>
> data Void
>         deriving(Typeable,Data,Eq,Ord,...) -- ^ a lot of valid classes
>                                            --   are defined for _|_
>
> fromVoid :: forall a . Void -> a
> fromVoid = unsafeCoerce#

as a bonus, with void, we get to be reminded of b-movie titles like

this friday, at your local theater:

"BEWARE! the catamorph from the VOID!"

I am not sure what a catamorph would be, depending on whether it is
preceded by cuddly or deadly I'd say a sidekick on thundercats or a
metamorphic feline killing machine.

speaking of which, there should be a contest among category theorists to
come up with the best definition for a 'Xenomorphism'. I am not sure
what it would be, but I doubt it would be structure preserving..

        John

--
John Meacham - ⑆repetae.net⑆john⑈
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Samuel Bronson
In reply to this post by John Meacham
On 10/23/06, John Meacham <[hidden email]> wrote:

> On Mon, Oct 23, 2006 at 05:17:49PM -0400, Samuel Bronson wrote:
> > On 10/23/06, John Meacham <[hidden email]> wrote:
> > >On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
> >
> > >data Bottom
> > Why not "data Void"?
>
> also good.
>
> or
>
> data Absurd
>
> also works for me.

Hmm, I like Absurd too ;-).
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Conor McBride
In reply to this post by Ashley Yakeley
Hi

Ashley Yakeley wrote:

> I wrote:
>
>>> magic :: Zero -> a
>>> magic _ = error "There's magic, as no such thing!"
>>
>> It's a little frustrating to have to define this function lazily. I
>> prefer the strict definition with no lines, but it isn't valid
>> Haskell!
>
> This issue comes up a lot with GADTs.

It's quite familiar with dependent types too, so that shouldn't come as
a surprise. Some of us have spent quite a while figuring out how to suck
a complete absence of eggs.

> For instance:
>
>   data MyGADT a where
>     MyInt :: MyGADT Int
>     MyChar :: MyGADT Char

or even

  data Eq a b where Refl :: Eq a a

  never :: Eq Int Bool -> a

In 'Eliminating Dependent Pattern Matching', Healf Goguen, James McKinna
and I suggest a notation which supplements the usual 'return an output'
notation with a 'refute an input' notation. Something like

  never x _|_ x  -- 'never x refutes x'

which requires x to be checkably in a type with no constructors (under
any hypotheses).

This notation enables a machine to check whether the programmer has
explained how to cover all cases by an explanation either of what to
return or why there's no need.

I wouldn't presume to propose this notation for Haskell, but equally,
it's dangerous to presume that as more and more of these phenomena show
up in Haskell, the old language choices will remain sufficient or suitable.

We live in interesting times.

All the best

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.

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Wolfram Kahl
In reply to this post by Samuel Bronson
Samuel Bronson <[hidden email]> wrote:
 >
 > On 10/23/06, John Meacham <[hidden email]> wrote:
 > > On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
 >
 > > data Bottom
 > Why not "data Void"?

I'd say that ``Void'' is not a desirable candidate
since too many people know C,
and the C type ``void'' corresponds to ``()'' (or ``IO ()''...)


(One name I have used before is ``Empty'', but I find ``Zero''
and ``Absurdity'' appropriate, too.
``Absurd'' perhaps sounds more like a value than like a type...)


Wolfram


_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Philippa Cowderoy
On Tue, 23 Oct 2006 [hidden email] wrote:

> Samuel Bronson <[hidden email]> wrote:
>  >
>  > On 10/23/06, John Meacham <[hidden email]> wrote:
>  > > On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
>  >
>  > > data Bottom
>  > Why not "data Void"?
>
> I'd say that ``Void'' is not a desirable candidate
> since too many people know C,
> and the C type ``void'' corresponds to ``()'' (or ``IO ()''...)
>

It doesn't, we just use () for similar things. You can't have a value of
type void in C - don't confuse a denotational semantics of C with C
itself.

--
[hidden email]

'In Ankh-Morpork even the shit have a street to itself...
 Truly this is a land of opportunity.' - Detritus, Men at Arms
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Donald Bruce Stewart
In reply to this post by Wolfram Kahl
kahl:

> Samuel Bronson <[hidden email]> wrote:
>  >
>  > On 10/23/06, John Meacham <[hidden email]> wrote:
>  > > On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
>  >
>  > > data Bottom
>  > Why not "data Void"?
>
> I'd say that ``Void'' is not a desirable candidate
> since too many people know C,
> and the C type ``void'' corresponds to ``()'' (or ``IO ()''...)
>
>
> (One name I have used before is ``Empty'', but I find ``Zero''
> and ``Absurdity'' appropriate, too.
> ``Absurd'' perhaps sounds more like a value than like a type...)
>

A precedent for Void comes from Djinn, http://darcs.augustsson.net/Darcs/Djinn,
well-known to #haskell irc people:

    Since Djinn handles propositional calculus it also knows about the
    absurd proposition, corresponding to the empty set.  This set is
    called Void in Haskell, and Djinn assumes an elimination rule for the
    Void type:

      data Void
      type Not x = x -> Void
      void :: Void -> a

    Using Void is of little use for programming, but can be interesting
    for theorem proving.  Example, the double negation of the law of
    excluded middle:

        Djinn> f ? Not (Not (Either x (Not x)))
          f :: Not (Not (Either x (Not x)))
            f x1 = void (x1 (Right (\ c23 -> void (x1 (Left c23)))))

I'd go so far as to say its intuitive to use Void, after the last year
spent playing with Djinn online.

-- Don
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Samuel Bronson
In reply to this post by Wolfram Kahl
On 23 Oct 2006 22:05:58 -0400, [hidden email]
<[hidden email]> wrote:

> I'd say that ``Void'' is not a desirable candidate
> since too many people know C,
> and the C type ``void'' corresponds to ``()'' (or ``IO ()''...)

So how come whenever I say that, someone invariably corrects me that
C's void type is uninhabited, whereas the () type is inhabited by ()?
And that a real void-alike wouldn't have any constructors?
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Philippa Cowderoy
On Mon, 23 Oct 2006, Samuel Bronson wrote:

> On 23 Oct 2006 22:05:58 -0400, [hidden email]
> <[hidden email]> wrote:
>
> > I'd say that ``Void'' is not a desirable candidate
> > since too many people know C,
> > and the C type ``void'' corresponds to ``()'' (or ``IO ()''...)
>
> So how come whenever I say that, someone invariably corrects me that
> C's void type is uninhabited, whereas the () type is inhabited by ()?
> And that a real void-alike wouldn't have any constructors?
>

Because C's an impure language - and thus it's possible to do something
meaningful without returning a value. Oh, and because they're right.

--
[hidden email]

The task of the academic is not to scale great
intellectual mountains, but to flatten them.
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Ashley Yakeley
Philippa Cowderoy wrote:

> On Mon, 23 Oct 2006, Samuel Bronson wrote:
>
>> On 23 Oct 2006 22:05:58 -0400, [hidden email]
>> <[hidden email]> wrote:
>>
>>> I'd say that ``Void'' is not a desirable candidate
>>> since too many people know C,
>>> and the C type ``void'' corresponds to ``()'' (or ``IO ()''...)
>> So how come whenever I say that, someone invariably corrects me that
>> C's void type is uninhabited, whereas the () type is inhabited by ()?
>> And that a real void-alike wouldn't have any constructors?
>>
>
> Because C's an impure language - and thus it's possible to do something
> meaningful without returning a value. Oh, and because they're right.

No, I think Wolfram's correct.

In C, void represents a return structure of zero bytes. It therefore has
256^0 = 1 value, just like the "()" type (ignoring bottom).

AFAIR C disallows declaring a variable void, though it would be
theoretically possible to relax this, and have them allocated as zero
bytes. Reading a variable of type "void" would return the "void value"
without actually reading from memory (since zero of it is allocated to
read from), and assigning to it would do nothing.

--
Ashley Yakeley


_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

ajb@spamcop.net
In reply to this post by John Meacham
G'day all.

Quoting John Meacham <[hidden email]>:

> 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.

Actually, this works fine.

data Zero
data Succ a

class Add a b c | a b -> c
instance Add Zero b b
instance (Add a b c) => Add (Succ a) b (Succ c)

It does smell like semantic overloading, though.

Cheers,
Andrew Bromage
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

Lennart Augustsson
In reply to this post by Samuel Bronson
Indeed, let's resurrect Void.  Haskell 1.4 had Void.  I never  
understood why it was removed.

        -- Lennart

On Oct 23, 2006, at 17:17 , Samuel Bronson wrote:

> On 10/23/06, John Meacham <[hidden email]> wrote:
>> On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
>
>> data Bottom
> Why not "data Void"?
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: A Pointless Library Proposal

roconnor
In reply to this post by Conor McBride
Conor McBride <ctm <at> Cs.Nott.AC.UK> writes:

> Elements of Zero are rather special, powerful things.
>
> > magic :: Zero -> a
> > magic _ = error "There's magic, as no such thing!"

Why have a function body at all?  Shouldn't the type signature be sufficent?

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
123