Permalink | Reply |
Permalink | Reply |
Permalink | Reply |
Permalink | Reply |
Permalink | Reply |
Permalink | Reply |
Permalink | Reply |
Brent Yorgey | 8 Dec 19:50 2011

Re: More liberal than liberal type synonyms

On Wed, Dec 07, 2011 at 04:47:47PM +0100, Gábor Lehel wrote:
> On Wed, Dec 7, 2011 at 1:07 PM, Dmitry Kulagin <dmitry.kulagin <at>> wrote:
> >> For short, type synonyms work for mere aliases, but not for full-fledged> type-level non-inductive
functions.> And sometimes we intuitively want to use them as such.
> > Thank you, Yves! It is now more clear for me.
> >
> > Still, it seems that ability to use partially applied type synonyms would be
> > very natural (and useful) extension to the language. It would allow to avoid
> > boilerplate code associated with creating "really new" types instead of just
> > using synonims for existing ones.
> The problem as I understand it is that partially-applied type synonyms
> are in effect type level lambdas, and type checking in the presence of
> type level lambdas requires higher-order unification, which is
> undecidable in general. Restricted cases might be possible, I'm not an
> expert in the field. GHC hackers could probably elaborate.
> [1]
> [2]

It's actually type *inference* that requires higher-order unification
in the presence of type-level lambdas, not type checking.  This might
not be a huge deal: we just have to clearly state that enabling
-XPartialTypeFunApps means that you may have to provide some explicit
type annotations in places where type inference cannot figure things
out.  We already have extensions like this (e.g. RankNTypes).

The bigger problem for the moment is that for various technical
reasons, enabling partial applications of type functions can lead to
(Continue reading)

Permalink | Reply |