RFC: Add HasCallStack constraint to partial Data.List functions.

[Carter Schonwald]

I feel like this brings up an idea I’ve been kicking around for a while and
maybe have suggested In the past in the context of exceptions:

We can have more info than just our vanilla type sigs in interface files.
Eg you could track approximate “may throw ” sets.  And one could conceive
of either module pragmas/function pragmas  or special built in combinators
that surface / help us reason about stuff!

One can go further ! You could imagine language modes that Eg surface
totality into how expresssions are typed in a module.

Or on the wacky end an impure strict language mode that converts all
expressions into left to right eval order Anf in the io monad and makes all
expressions essentially do notation for the io monad!

The point I’m trying to illustrate and articulate by example is that while
every flavor of reasoning can have a type theoretic embedding, that doesn’t
mean everyone else has to see or work with those cosntraints!

A slightly real example of this in ghc today is how we supresss levity
polymorphism in types by default for users.

So how can we cook up some tools that allow these sorts of information to
be visible to those who want it and invisible to those who don’t?

I sometimes wonder if, were we designing the ghc abi/calling  convention
today, would we have a register reserved for the analogue of the has call
stack info? (I suppose the dwarf info and stack walking tools on ELF
platforms is that to some extent. Just sadly not on all platforms in tier 1
:(. )

On Tue, Jun 8, 2021 at 2:29 PM David Feuer <david.feuer at gmail.com> wrote:

> On Tue, Jun 8, 2021, 1:39 PM Richard Eisenberg <lists at richarde.dev> wrote:
>
>> I've been very much of two minds in this debate: On the one hand, having
>> these constraints is very practically useful. On the other, what we're
>> doing here is very un-Haskellish, in that we're letting operational
>> concerns leak into a declarative property (a function's type).
>>
>
> Yes, this is quite awkward. We have here a tension:
>
> 1. The *operational* type, indicating the calling convention. This
> includes HasCallStack.
>
> 2. The "denotational" type (for want of a better term), indicating what
> users (generally) have to know about the function. This does not include
> HasCallStack.
>
> HasCallStack is already partially magical (and the rest is library
> internals). Maybe we should take that further, and remove HasCallStack from
> type signatures. Pardon my fake syntax:
>
> error :: forall {rep} (a :: TYPE rep). String -> a
> error @(_ :: class HasCallStack) msg = ...
>
> head :: [a] -> a
> head @(_ :: class HasCallStack) [] = error ...
>
> This has two downsides I see:
>
> 1. It's no longer so easy to tell whether a function takes a call stack.
> But that's kind of the point; we usually don't want to think about that.
> 2. It's no longer so obvious that undefined is a function. But ... we very
> rarely care that it is.
>
>> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20210608/7b5493b3/attachment.html>