[Haskell-cafe] Injective type families for GHC - syntax proposals

[Jay Sulzberger]

On Wed, 17 Sep 2014, Jan Stolarek <jan.stolarek at p.lodz.pl> wrote:

> Haskellers,
>
> there is some discussion going on at the moment about implementing injective
> type families in GHC [1]. I'd like to hear your opinions on proposed syntax for this
> new feature.

As an old Lisper I look forward to an all sexp version of Haskell
source code.  I do note your ':-)' below ;)

oo--JS.

>
> == Problem ==
>
> Currently GHC assumes that type families are not injective. This is of course
> conservative and the idea behind implementing injective type families is to
> allow the programmer to explicitly declare that a type family has the
> injectivity property (which GHC will of course verify).
>
> == Forms of injectivity ==
>
> Injectivity can take forms more complicated than just determining the LHS from
> RHS:
>
> A. RHS determines all arguments on the LHS. Example:
>
>   type family Id a where
>        Id a = a
>
>   Here the RHS uniquely determines LHS.
>
> B. RHS determines some but not all arguments on the LHS. Example (contrieved):
>
>   type family G a b c where
>        G Int  Char Bool = Bool
>        G Int  Char Int  = Bool
>        G Bool Int  Int  = Int
>
>   Here RHS uniquely determines `a` and `b` but not `c`.
>
> C. RHS and some LHS arguments uniquely determine some LHS arguments. Example:
>
>   type family Plus a b where
>        Plus Z     m = m
>        Plus (S n) m = S (Plus n m)
>
>   Here knowing the RHS and one of LHS arguments uniqely determines the other
>   LHS argument.
>
> At the moment we've only seen use cases for A, which means that we will most likely only
> implement A. If someone comes up with compelling examples of either B or C we
> will revise and consider implementing these more involved forms of injectivity.
>
>
> == Syntax ==
>
> So the most important decission to make is what syntax do we want for this new
> feature :-) One of the features we would like is extensibility, ie. if we only
> implement injectivity of type A we still want to be able to add injectivities B
> and C sometime in the future without breaking A.
>
> When thinking about syntax an important (and open) question is whether
> injectivity becomes part of TypeFamilies language extension or do we add a new
> InjectiveTypeFamilies extension for this feature. The problem with incorporating
> injectivity into existing TypeFamilies is that we would have to come up with
> syntax that is fully backwards compatible with what we have now.
>
> Below is a list of proposals that have come up until now in the discussion
> between developers. Note that all proposals are given for closed type families.
> For open type families things would be identical except that the `where` keyword
> would be skipped.
>
>
> === Proposal 1 ===
>
> Use syntax similar to functional dependencies. The injectivity declaration
> begins with `|` following type family declaration head. `|` is followed by a
> list of comma-separated injectivity conditions. Each injectivity condition has
> the form:
>
> {{{
> result A -> B
> }}}
>
> where `A` is a possibly-empty list of type variables declared in type family
> head and `B` is non-empty list of said type variables. Things on the left and
> right of `->` are called LHS and RHS of an injectivity condition,
> respectively. `result` becomes a restricted word that cannot be used as a type
> variable's identifier in a type family head. Examples:
>
>   type family Id a | result -> a where
>   type family G a b c | result -> a b where
>   type family Plus a b | result a -> b, result b -> a where
>
> Pros:
>
>  * has natural reading: `result a -> b` reads as "knowing the result and the
>    type variable a determines b".
>
>  * extensible for the future
>
> Cons:
>
>  * steals `result` identifier in the type family head. This means it would be
>    illegal to have a type variable named `result` in a type family.
>
>  * the above also makes this proposal backwards incompatible with TypeFamilies
>    extension.
>
> Further proposals are based on this one in an attempt to solve the problem of
> stealing syntax and backwards incompatibility.
>
>
> === Proposal 2 ===
>
> Use `Result` instead of `result`:
>
>   type family Id a | Result -> a where
>   type family G a b c | Result -> a b where
>   type family Plus a b | Result a -> b, Result b -> a where
>
> Pros:
>
>  * has natural reading
>
>  * extensible for the future
>
>  * allows to have type variables named `result` (does not steal syntax)
>
> Cons:
>
>  * all other keywords in Haskell are lowercase. This would be the first one
>    that is capitalized.
>
>  * confusion could arise if we have a type `Result` and use it in the type
>    family head.
>
> Unknowns (for me):
>
>  * not sure if it would be possible to avoid name clash between `Result` and
>    type of the same name. If not then this proposal would also be backwards
>    incompatible with TypeFamilies.
>
>
> === Proposal 3 ===
>
> Use `type` instead of `result`:
>
>   type family Id a | type -> a where
>   type family G a b c | type -> a b where
>   type family Plus a b | type a -> b, type b -> a where
>
> Pros:
>
>  * extensible for the future
>
>  * no syntax stealing
>
> Cons:
>
>  * no natural reading
>
>  * usage of `type` here might seem unintuitive
>
>
> === Proposal 4 ===
>
> Use name of the type family instead of `result`:
>
>   type family Id a | Id -> a where
>   type family G a b c | G -> a b where
>   type family Plus a b | Plus a -> b, Plus b -> a where
>
> Pros:
>
>  * extensible for the future
>
>  * no syntax stealing
>
> Cons:
>
>  * writing something like `Plus a` might be confusing. It looks as if Plus
>    could be partially applied.
>
>
> == Further discussion ==
>
> I'd like to hear what you think about these proposals. Neither of them is
> perfect so perhaps someone can come with something better. You can also check
> out the GHC Trac ticket [1] and the GHC Wiki page [2] (which repeats most of this but has some
> more details as well).
>
> [1] https://ghc.haskell.org/trac/ghc/ticket/6018
> [2] https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies
>
> Janek
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>