<div dir="auto">FWIW, partiality annotations seem a bit silly to me when we don't have termination checking.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jun 9, 2021, 9:45 AM Henrik Nilsson <<a href="mailto:Henrik.Nilsson@nottingham.ac.uk">Henrik.Nilsson@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> > I'm not sure I really agree with that.  There is a rich literature on <br>
 > effect systems, which decorate types with information about what<br>
 > effects the function has: exceptions, divergence, IO, and the like. <br>
  > So type like<br>
 >   head :: Partial => [a] -> a<br>
 > where 'Partial =>' expresses the fact that calling this function<br>
 > might lead to a call of 'error' doesn't seem inherently something<br>
 > that doesn't belong in a type system.<br>
<br>
I, of course, agree that partiality is an effect. And I have no<br>
issues with effects being reflected in the type system.<br>
We do that all the time with e.g. monads.<br>
<br>
If we indeed had something like<br>
<br>
    head :: Partial => [a] -> a<br>
<br>
that would be both informative and fairly straightforward to<br>
explain to students, for example. (Even if it is not clear to<br>
me that a type class really is the right way to express<br>
partiality of functions: I always thought information about<br>
partiality ought to be tied to the function arrow.)<br>
<br>
My point is that "HasCallStack" strongly suggest a specific approach<br>
to monitor the behaviour of a function in case it goes wrong.<br>
<br>
To me, at least, that is very operational.<br>
<br>
And I would struggle to explain<br>
<br>
    head :: HasCallStack => [a] -> a<br>
<br>
beyond saying "it's just something that sometimes will help you<br>
with debugging", and deeply hoping no clever student would<br>
ask about the lack of similar annotations for other partial<br>
functions.<br>
<br>
Best,<br>
<br>
/Henrik<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please contact the sender and delete the email and<br>
attachment. <br>
<br>
Any views or opinions expressed by the author of this email do not<br>
necessarily reflect the views of the University of Nottingham. Email<br>
communications with the University of Nottingham may be monitored <br>
where permitted by law.<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>