Proposal: add `Prelude.todo :: a`

#1

@MangoIV raised a proposal to add Prelude.todo :: a which is undefined is disguise with a custom warning attached: {-# WARNING in "x-todo" todo "todo remains in code" #-}.

Judging from the number of upvotes, the proposal addresses an important pain point, yet comments express certain reluctance to extend Prelude. Are we missing any alternatives? Is the balance of pros and cons assessed correctly? I feel that the discussion can benefit from comments and opinions of a wider audience.

I’m raising this topic here to increase visibility, but please comment at Add the `todo` function · Issue #260 · haskell/core-libraries-committee · GitHub if you can.

11 Likes
#2

…yes, @MangoIV raised it here too:

Adding something like todo :: a to the Prelude would go against the trend towards totality in Haskell - I can’t find it right now, but someone recently bemoaned the existence of Prelude.error …

1 Like
#3

Great initiative! The clearer semantics will definitely help adoption.

2 Likes
#4

Adding something like todo :: a to the Prelude would go against the trend towards totality in Haskel

I don’t see it that way, since todo is not supposed to be part of any finished program. I think it is more a reflection of the trend away from batch compilation to interactions and a dialogue with the compiler. Therefore it is important to not only consider the semantics of complete programs but also for programs “in the making”.

11 Likes
#5

That’s actually a great point! Could you perhaps add that to the issue?

#6

Many people here also think that head and tail are not supposed to be part of any finished program - make of that what you will :-)

…I’m now intrigued - considering the ongoing transition of (Glasgow) Haskell towards dependent typing, would the need for some level of totality (so that proofs can actually be useful) conflict in some way with such an incremental approach?

1 Like
#7

I don’t think that the concern for incomplete programs conflicts with the goal of dependent types. On the contrary, it is almost impossible to write dependent programs without constant help from the compiler, so the semantics of incomplete programs is even more important for dependently typed programs. (And the reason why hole-based programming is much more prevalent in Agda and Idris). Coq, for example, doesn’t provide anything like “undefined” in its Core library afaik, so I always have the following definition in all of my projects :sweat_smile:

Definition undefined {A : Prop} :A.
 admit.
Admitted.

This is not a problem for the typechecker, since it just blocks on evaluation instead of diverging.

1 Like
#8

Additionally, dependent typing, especially in the case of Haskell, doesn’t have to and won’t mean totality.

#9

Before the aforementioned transition, an analogous remark could have been made about dependent typing e.g:

In addition, [various Haskell type extensions] especially in the case of Haskell, doesn’t have to and won’t mean dependent typing.

…but here we all are.

Getting back on-topic: mixphix’s examination of your proposal here seems quite thorough to me - this point is particularly compelling:

This [removing the dependency on todo] is impossible should todo be exported from base, eliminating any such guarantee.

If todo was in the Prelude, then it seems the only way to remove that dependency would be to add the following to each and every Haskell module in the entire codebase:

import Prelude hiding (todo)

…which is utterly impractical, compared to just removing e.g. todo from the codebase’s package-dependency list.

Assuming it’s correct, then based on that observation DavidB’s suggested alternative here seems the better option - it looks like a comparatively-small change to GHC; one that can be easily reversed later if necessary e.g. because it caused too many naming conflicts.

#10

I wouldn’t mind having this is a standalone package or base module tbh

Although module causes the same issues. Pretty annoying how it’s impossible to add symbols to Prelude or base without a backwards compat discussion each time lol.

Luckily, this one seems pretty safe.

#11

Do try to remember that cheery sentiment when a “flag day” upgrade is required in one or more of your codebases…

Well, no-one (usually) goes out of their way to deliberately add blatantly-bad features…

2 Likes
#12

I was going to comment on this on Github, but my Github account is temporarily disabled as my phone connection is out of order.

If you Hoogle todo and use the synonym TODO in Serokell’s service, you’ll see that there’s a lot of codebase clashes, including in the latter case, comments.

Moreover, in Portuguese, it seems that “todo” also means all, which could trigger confusion for a small number of Lusophone users.

While TODO is probably the most eye-catching solution, I’d suggest a pattern synonym of ToDo, which does not show up in Hoogle, is distinct from usage of TODO in codebase comments, and is clearly connotes different meaning from the Portuguese due to its eccentric capitalization.

I’d also suggest that ToDo is sufficiently irritating (what is this, MySpace?) that it will cause a compulsion to finish your projects. :slight_smile:

See:

https://hackage-search.serokell.io/?q=^TODO

Well, ToDo isn’t perfect either:

https://hackage-search.serokell.io/?q=^ToDo

But it’s 800 matches vs 137, and I’d imagine it’s easier to switch comments to TODO instead of ToDo in the long-term.

#13

Maybe it is better to have todo not in Prelude, but on own module, like Control.Todo or Debug.Todo

4 Likes
#14

But then to check that they’ve all been done, imports of $SOURCE_MODULE.todo would have to be removed from each Haskell module which uses it. That might be alright for a few Haskell modules, but for an entire codebase full of Haskell modules? That seems rather unwieldy, in comparison to just removing a single package dependency e.g. on todo…

1 Like
#15

Makes sense - we already import Debug.Trace all the time. This feels similar.

2 Likes