<div dir="ltr">Even with "ReallyLiberalTypeSynonyms" you can't have (f . g) ~ h as that would involve a partial application in a non type synonym, so there is no issue with unification.<div><br></div><div>(.) only means something with all 3 arguments applied so that it can be expanded, but you can still allow it to be formally passed around inside other type synonyms so long as the final type synonym has all of its arguments expanded.</div><div><br></div><div>type (.) f g x = f (g x)</div><div>type Foo = (.) Bar</div><div><br></div><div>Foo doesn't fully instantiate (.) but you can keep eta expanding it until it does.</div><div><br></div><div>type Foo g x = (.) Bar g x = Bar (g x)</div><div><br></div><div>is a perfectly legitimate definition. You can do this expansion automatically pretty easily. Given such a type synonym you can answer how many arguments it must have before it is a real type.</div><div><br></div><div>At a use site Foo is not a type until it has been applied to two more arguments, just like the eta expanded form above. Foo ~ Baz doesn't type check for the same reason given </div><div><br></div><div>type Id a = a</div><div><br></div><div><div>you can't talk about Id ~ Bar. Id isn't a type. It needs an argument before it makes sense.</div></div><div><br></div><div>This is what I mean by "ReallyLiberalTypeSynonyms". We actually wound up with these by accident in the Ermine compiler we use at work, and they turned out to be quite useful and harmless in practice.</div><div><br></div><div>We don't have this power today, but we do have LiberalTypeSynonyms, which gets us close.</div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Nov 2, 2016 at 7:36 PM, Ken Bateman <span dir="ltr"><<a href="mailto:novadenizen@gmail.com" target="_blank">novadenizen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">Wouldn't there also be a problem with type unification? When unifying ((f . g) a) and (h b) do you set ((f . g) ~ h) or ((g a) ~ b)?</p><div class="HOEnZb"><div class="h5">
<div class="gmail_extra"><br><div class="gmail_quote">On Nov 2, 2016 6:28 PM, "Edward Kmett" <<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>On Wed, Nov 2, 2016 at 3:11 PM, Index Int <span dir="ltr"><<a href="mailto:vlad.z.4096@gmail.com" target="_blank">vlad.z.4096@gmail.com</a>></span> wrote:<br></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Edward, I don't quite follow why you think that (.) is needed here.<br>
Monad transformers take two parameters, so your example is not<br>
type-correct, whereas the original one is.<br></blockquote><div><br></div><div>Indeed, I appear to have hyper-corrected that example.</div><div><br></div><div>-Edward</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="m_-568975434242063835m_-3250282368172279798gmail-HOEnZb"><div class="m_-568975434242063835m_-3250282368172279798gmail-h5">
On Wed, Nov 2, 2016 at 5:24 PM, Edward Kmett <<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>> wrote:<br>
> +1, but the operator you're looking for in App there would actually be a<br>
> type level version of (.).<br>
><br>
> type App a = ExceptT Err $ ReaderT Config $ LogT Text $ IO a<br>
><br>
> type App = ExceptT Err . ReaderT Config . LogT Text . IO<br>
><br>
> which would need<br>
><br>
> type (.) f g x = f (g x)<br>
> infixr 9 .<br>
><br>
> to parse<br>
><br>
> -Edward<br>
><br>
> On Tue, Nov 1, 2016 at 7:13 PM, Elliot Cameron <<a href="mailto:eacameron@gmail.com" target="_blank">eacameron@gmail.com</a>> wrote:<br>
>><br>
>> Folks,<br>
>><br>
>> Has there been a discussion about adding a type-level operator "$" that<br>
>> just mimics "$" at the value level?<br>
>><br>
>> type f $ x = f x<br>
>> infixr 0 $<br>
>><br>
>> Things like monad transformer stacks would look more "stack-like" with<br>
>> this:<br>
>><br>
>> type App = ExceptT Err $ ReaderT Config $ LogT Text IO<br>
>><br>
>> Elliot Cameron<br>
>><br>
>> ______________________________<wbr>_________________<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-bi<wbr>n/mailman/listinfo/libraries</a><br>
>><br>
><br>
><br>
> ______________________________<wbr>_________________<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-bi<wbr>n/mailman/listinfo/libraries</a><br>
><br>
</div></div></blockquote></div><br></div></div>
<br>______________________________<wbr>_________________<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-bi<wbr>n/mailman/listinfo/libraries</a><br>
<br></blockquote></div></div>
</div></div></blockquote></div><br></div>