<div dir="auto">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:</div><div dir="auto"><br></div><div dir="auto">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!</div><div dir="auto"><br></div><div dir="auto">One can go further ! You could imagine language modes that Eg surface totality into how expresssions are typed in a module.  </div><div dir="auto"><br></div><div dir="auto">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!</div><div dir="auto"><br></div><div dir="auto">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!</div><div dir="auto"><br></div><div dir="auto">A slightly real example of this in ghc today is how we supresss levity polymorphism in types by default for users. </div><div dir="auto"><br></div><div dir="auto">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? </div><div dir="auto"><br></div><div dir="auto">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 :(. )</div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Jun 8, 2021 at 2:29 PM David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Jun 8, 2021, 1:39 PM Richard Eisenberg <<a href="mailto:lists@richarde.dev" target="_blank">lists@richarde.dev</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space">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).</div></blockquote></div></div><div dir="auto"><br></div><div dir="auto">Yes, this is quite awkward. We have here a tension:</div><div dir="auto"><br></div><div dir="auto">1. The *operational* type, indicating the calling convention. This includes HasCallStack.</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">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:</div><div dir="auto"><br></div><div dir="auto">error :: forall {rep} (a :: TYPE rep). String -> a</div><div dir="auto">error @(_ :: class HasCallStack) msg = ...</div><div dir="auto"><br></div><div dir="auto">head :: [a] -> a</div><div dir="auto">head @(_ :: class HasCallStack) [] = error ...</div><div dir="auto"><br></div><div dir="auto">This has two downsides I see:</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto">2. It's no longer so obvious that undefined is a function. But ... we very rarely care that it is.</div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
</blockquote></div></div></div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div>