On 10/23/06, John Meacham wrote:

On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:

data Bottom Why not "data Void"?

On Monday 23 October 2006 17:26, Jason Dagit wrote:

On 10/23/06, Samuel Bronson wrote:

...

On 10/23/06, John Meacham 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

On 10/23/06, John Meacham wrote:

On Mon, Oct 23, 2006 at 05:17:49PM -0400, Samuel Bronson wrote:

...

On 10/23/06, John Meacham 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 ;-).

On Tue, 23 Oct 2006 kahl@cas.mcmaster.ca wrote:

Samuel Bronson wrote:

...

On 10/23/06, John Meacham 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. -- flippa@flippac.org 'In Ankh-Morpork even the shit have a street to itself... Truly this is a land of opportunity.' - Detritus, Men at Arms

On 23 Oct 2006 22:05:58 -0400, kahl@cas.mcmaster.ca 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?

Philippa Cowderoy wrote:

On Mon, 23 Oct 2006, Samuel Bronson wrote:

...

On 23 Oct 2006 22:05:58 -0400, kahl@cas.mcmaster.ca 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

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.

G'day all. Quoting John Meacham :

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

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.

Samuel Bronson writes:

On 10/24/06, Russell O'Connor wrote:

...

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

Remember that type signatures need not be adjacent to function definitions. Now ponder what would happen if you forgot to define a function. Have a clue why it isn't sufficient now?

If you turn on -Wall in GHC, you would get a warning that your pattern coverage is incomplete. We should make it so that if the pattern coverage is incomplete and there is no function body, then that is an error.

Hi Russell O'Connor wrote:

Samuel Bronson writes:

...

On 10/24/06, Russell O'Connor wrote:

...

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

Hmmm

...

Remember that type signatures need not be adjacent to function definitions. Now ponder what would happen if you forgot to define a function. Have a clue why it isn't sufficient now?

If you turn on -Wall in GHC, you would get a warning that your pattern coverage is incomplete. We should make it so that if the pattern coverage is incomplete and there is no function body, then that is an error.

So, taking Void to be the colour of the empty bikeshed and avoid :: Void -> x suppose I define data WrapVoid = Wrap Void may I now write boo :: WrapVoid -> x with no equations? Does this cover? Or does it neglect the crucial boo (Wrap _|_) case? What about hoo :: Void -> Bool -> x ? Does this cover, or did I forget hoo v True and hoo v False? Funny business, coverage checking. With GADTs, things become even more entertaining... All the best Conor

Hi again [editing slightly] Russell O'Connor wrote:

Conor McBride writes:

...

may I now write

boo :: WrapVoid -> x hoo :: Void -> Bool -> x

with no equations? It would be considered ``covered''; however you may, at your option, wish to add function body to handle (Wrap x).

This is considered covered, but again you may, at your option, wish to add a function body to handle the hoo v True and hoo v False cases.

Hmmm. For GADTs, I fear that this coverage checking problem may be undecidable. To see why, check page 179 of my PhD thesis, although the result (due to Gerard Huet, I believe) was certainly known to Thierry Coquand in 1992. But...

Basically we considered all the cases covered if they are covered for all non-bottom values. This is (I understand) what the warning in GHC does.

...isn't (Wrap _|_) a non-bottom value? Doesn't moo (Wrap v) = True distinguish (Wrap _|_) from _|_ ? If you're willing to tolerate the need to cover these cases, coverage checking becomes decidable! Of course, it leaves you wondering what to write on the right-hand side...

I would also be willing to consider Christian Maeder's proposal where a missing function body is never an error.

I'd be more comfortable with a more explicit way to leave a stub, but I agree that there should be a way to indicate 'unfinished' which is distinct from 'defined to be _|_'. Moreover, I should very much like to have a token I can write in the place of an expression, such that on compilation, I receive a diagnostic giving me as much type information as possible about what must replace the token. When you try the old trick of making a deliberate type error to achive this effect, you often get less back than you might hope. Fine for genuine errors, but not enough to satisfy the ulterior motive. Cheers Conor

On Oct 25, 2006, at 5:24 AM, Conor McBride wrote:

Hi again

[editing slightly]

Russell O'Connor wrote:

...

Conor McBride writes:

...

may I now write

boo :: WrapVoid -> x hoo :: Void -> Bool -> x

with no equations? It would be considered ``covered''; however you may, at your option, wish to add function body to handle (Wrap x). This is considered covered, but again you may, at your option, wish to add a function body to handle the hoo v True and hoo v False cases.

Hmmm. For GADTs, I fear that this coverage checking problem may be undecidable. To see why, check page 179 of my PhD thesis, although the result (due to Gerard Huet, I believe) was certainly known to Thierry Coquand in 1992. But...

...

Basically we considered all the cases covered if they are covered for all non-bottom values. This is (I understand) what the warning in GHC does.

...isn't (Wrap _|_) a non-bottom value? Doesn't

moo (Wrap v) = True

distinguish (Wrap _|_) from _|_ ?

If you're willing to tolerate the need to cover these cases, coverage checking becomes decidable! Of course, it leaves you wondering what to write on the right-hand side...

...

I would also be willing to consider Christian Maeder's proposal where a missing function body is never an error.

I'd be more comfortable with a more explicit way to leave a stub, but I agree that there should be a way to indicate 'unfinished' which is distinct from 'defined to be _|_'.

I'd have to say that all we really need for the original problem is a case statement with no arms. eg, data Void void :: Void -> a void x = case x of {} However, I feel this whole conversation is pretty academic because void x = undefined has exactly the same semantics, and void x = x `seq` undefined will even have pretty much the same operational behavior. I agree that being able to directly implement the Void catamorphism is appealing, I just don't think it makes a big practical difference. I would not at all like to see the ability to define functions by just writing type signatures.

Moreover, I should very much like to have a token I can write in the place of an expression, such that on compilation, I receive a diagnostic giving me as much type information as possible about what must replace the token. When you try the old trick of making a deliberate type error to achive this effect, you often get less back than you might hope. Fine for genuine errors, but not enough to satisfy the ulterior motive.

Cheers

Conor

Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG

Hi David Menendez wrote:

Conor McBride writes:

...

...

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!

I think you could avoid that frustration by defining Zero/Void/Bikeshed liko so:

newtype Void = Void { avoid :: forall a. a }

That gets you a strictly defined avoid and emphasizes that Void is isomorphic to (forall a. a).

Aha, the Church Void! That's a neat way of doing it under the circumstances. The datatype with no constructors issue will show up again with GADTs, but this is a sensible way to postpone it. I guess (to answer Rob Dockins) that it's not the number of lines I'm bothered by, but rather the invocation of 'undefined', 'error' or some other signal of /underdefinition/ to present a function which is entirely well-defined, indeed trivially so. This may seem academic, but with types being used increasingly in their role as evidence, we'll eventually need to be comfortable with negative information as well as positive.

On a semi-related note, how about instances for the Prelude classes?

For example,

instance Show Void where show = avoid

instance Read Void where readsPrec _ _ = []

instance Eq Void where a == b = avoid a

instance Ord Void where compare a b = avoid a

Absolutely! It's not a joke. Some notion of Zero (and here's really why I like Zero) is very useful if you're doing algebra, let alone calculus with data structures. Given how many of our favourite datatypes are fixpoints of polynomial functors, with Show, Eq, etc, it's important that each of the building blocks of polynomials is closed under these things. You might not often need to use a Zero in the polynomial datatypes you define, but it's useful to have Zero if you're calculating one polynomial from another. I want to get for free that if my datatype has polynomial nodes, its type of one-hole contexts is showable. All the best Conor

| I don't like this idea because the necessary stub is different for different | numbers of arguments, and there's no way to tell how many arguments the | programmer intended. Why? What's wrong with expanding foo :: Int -> Int -> Int into foo :: Int -> Int -> Int foo = error "foo is not yet implemented" which is what I usually write by hand. |I do like the idea of allowing empty case expressions, | though, and I don't think that even a warning would be necessary. So how would you define foo? How would it be better than the above (even if written by hand)? Simon

On Mon, Oct 30, 2006 at 10:16:46AM -0500, Lennart Augustsson wrote:

I like to use undefined is the stub for unimplemented functions since it's nice and terse. Unfortunately, ghc doesn't give much information about where the undefined was called. It would be great if the message for undefined could include file name and line number (like hbc did :).

jhc has the SRCLOC_ANNOTATE pragma, which lets you attach file and line number information to arbitrary functions. sort of a generalization of the 'assert' feature of ghc. One day I will get around to implementing it in ghc. perhaps the next time a program I write mysteriously dies with "Prelude.undefined" being the only thing printed. John -- John Meacham - ⑆repetae.net⑆john⑈

On 31/10/06, Donald Bruce Stewart wrote:

But seems like we need a 'proper' solution. undefineds with lines numbers, and errors with line numbers, would be a good start.

I think it'd be nice to keep undefined around as a 'pure' bottom, and introduce a new value, say 'stub :: forall a. a' which is magic and sends the file and line location of its mention to stderr when executed. -- -David House, dmhouse@gmail.com

Hello David, Tuesday, October 31, 2006, 1:20:42 PM, you wrote:

...

But seems like we need a 'proper' solution. undefineds with lines numbers, and errors with line numbers, would be a good start.

I think it'd be nice to keep undefined around as a 'pure' bottom, and introduce a new value, say 'stub :: forall a. a' which is magic and sends the file and line location of its mention to stderr when executed.

and then you will introduce exception handling? :) i think that 'undefined' should be not function but preprocessor symbol that's translated into "file:line" notation, and we need the same symbol for monads while error/fail should be used for custom error messages (as they currently used) -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

On Oct 30, 2006, at 9:38 AM, Ben Rudiak-Gould wrote:

Simon Peyton-Jones wrote:

...

I've occasionally wondered about emitting a warning, but not an error, when there's a type signature for a function but no definition. The compiler could automatically generate an error message stub implementation, much as it does for an incomplete pattern match, of which this is an extreme example.

I don't like this idea because the necessary stub is different for different numbers of arguments, and there's no way to tell how many arguments the programmer intended. I do like the idea of allowing empty case expressions, though, and I don't think that even a warning would be necessary.

This opinion++

-- Ben

Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG