<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
On 2017-05-07 05:19, Theodore Lief Gannon wrote:<br>
<blockquote
cite="mid:CAJoPsuB_Etno89WGN4P3sHk6LfM5OBOfOcqCkTnMLymK=Q5uwQ@mail.gmail.com"
type="cite">
<div dir="ltr">
<div>Namespace notation might not be optimal, because it's not
clear at a glance that this is an aspect and not a regular
qualified import of a type (an important distinction if you
have multiple versions of the same type imported, e.g.
Bytestring). Why not make it look like type application
instead? Modifying your example:</div>
<div>
<pre style="white-space:pre-wrap">allEven :: (Integral a) => [a] -> Bool@A_All_</pre>
</div>
<div>And for that matter, I'd rather not be forced to write a
signature (what if I want to use this in a <font
face="monospace, monospace">where</font> clause?) So... does
this break anything?<br>
</div>
<div>
<pre style="white-space:pre-wrap">allEven = foldMap@A_All_ even</pre>
<pre style="white-space:pre-wrap"><font face="arial, helvetica, sans-serif">Which means, for this invocation of </font><font face="monospace, monospace">foldMap</font><font face="arial, helvetica, sans-serif">, instances within </font><font face="monospace, monospace">A_All_</font><font face="arial, helvetica, sans-serif"> are in effect for all of its constraints. You could chain multiple </font><font face="monospace, monospace">@</font><font face="arial, helvetica, sans-serif">'s together so long as they don't produce any relevant overlapping instances.</font>
</pre>
</div>
</div>
</blockquote>
<p>Good point, and it brought up some interesting follow-up
thoughts. First of all I like this "annotative" notation vs
stating aspects in constraints. The main reason is that the latter
would make type signatures even worse:</p>
<pre style="white-space:pre-wrap"> allEven :: (Integral a, b ~ Bool, HasAspect A_All_ b) => [a] -> b</pre>
<p>But before I go on, let's first introduce better names and start
at<br>
</p>
<pre style="white-space:pre-wrap"> allEven :: (Integral a) => [a] -> Bool@Conjunctive</pre>
<p> At first glance I thought your suggested notation might clash
with TypeApplication. But then I noticed that no, it's actually
more of a TypeAnnotation-like kind annotation. That might mean
that this exact syntax should stay untouched in case we want some
more general kind annotations later. So maybe something like this
with a different operator? Another conclusion of that is that
maybe we would want to apply aspect annotations inside
TypeAnnotations. I imagine that might look something like <tt>(Maybe
@Bool@Disjunctive)</tt>. So the @ sign does make sense.
Combining both thoughts, maybe an operator like "@+" would be
best, because in a way the aspect is added to the type. And if
other kind applications should be added later they could still use
the @. So to step outside of TypeApplication again, the example
would now look something like</p>
<pre style="white-space:pre-wrap"> allEven :: (Integral a) => [a] -> Bool @+Conjunctive
</pre>
<p>or, to keep the function signature clean<br>
</p>
<pre style="white-space:pre-wrap"> allEven :: (Integral a) => [a] -> Bool
allEven = (foldMap even) :: Bool @+Conjunctive
</pre>
<p>Maybe there's some way to save a few bytes in this case like<br>
</p>
<pre style="white-space:pre-wrap"> allEven :: (Integral a) => [a] -> Bool
allEven = foldMap even :: @@+Conjunctive -- a step back to TypeApplication</pre>
<p>Chaining several aspects would be straightforward: <tt>(Bool
@+Disjunctive@+Conjunctive</tt><tt>)</tt> (here it produces a
conflict), <tt>(Maybe @a@+Multiplicative@+Distributive)</tt> etc.<br>
</p>
<p>Looking at this as a type with an operator leads in yet a
completely different direction: Could part of this already be
implemented via type families? Sadly not, for two reasons. Most
importantly instances can not be hidden. To change that might be
the most powerful result of this whole idea. The other part is
also interesting. If "@+" was a type-level operator, its second
argument would have to be an aspect. And seeing how aspects would
be more or less restricted modules, this would open the question
if modules should have a representation as a kind as well, the
same way constraints do. I think that sounds really interesting.
But neither aspects nor modules make sense as kinds until we also
have some type level tools to work with them. Apart from those
tools we would need here I have little idea what such tools might
be, but it sounds worth exploring separately. For this particular
proposal my conclusion is just that the implementation would have
to be easy to adapt.</p>
The only part I don't like about this compared to just abusing
namespace notation is that it would introduce yet another syntax
element. And what's worse, one that interacts with parts of the
syntax I'm not too familiar with and that are relatively new and
experimental as far as I understand (TypeApplication).<br>
<br>
<blockquote
cite="mid:CAJoPsuB_Etno89WGN4P3sHk6LfM5OBOfOcqCkTnMLymK=Q5uwQ@mail.gmail.com"
type="cite">
<div dir="ltr">
<div>
<pre style="white-space:pre-wrap"><font face="arial, helvetica, sans-serif">To avoid surprises, they shouldn't propagate -- when </font><font face="monospace, monospace">foldMap</font><font face="arial, helvetica, sans-serif"> invokes </font><font face="monospace, monospace">even</font><font face="arial, helvetica, sans-serif">, it sees the default </font><font face="monospace, monospace">Monoid</font><font face="arial, helvetica, sans-serif"> instance for </font><font face="monospace, monospace">Bool</font><font face="arial, helvetica, sans-serif"> (i.e. none). If it were also a function that needs a </font><font face="monospace, monospace">Monoid</font><font face="arial, helvetica, sans-serif">, you'd need another </font><font face="monospace, monospace">@</font><font face="arial, helvetica, sans-serif">. There's potential for boilerplate here. Falling back to doing it in the type signature could force propagation? I'm not sure it's ever a safe idea, though.</font></pre>
</div>
</div>
</blockquote>
<p>That sounds like a gateway to inconsistency. I think the solution
is that adding an aspect to, say, an Int would not apply that
aspects to all Int's, but only to the ones unifying with the
annotated one. So just like with any other type property. Or to
tie this back to the beginning, I suppose the notation we're
discussing here should actually just be syntactic sugar for
something constraint-related. All propagation rules would follow
from that in a natural fashion.<br>
</p>
<p>So much to think about…</p>
<p>Cheers,<br>
MarLinn<br>
</p>
</body>
</html>