[Haskell-cafe] Injective type families for GHC - syntax proposals
Jason McCarty
jmccarty at sent.com
Wed Sep 17 18:54:57 UTC 2014
Hi,
I have some code that currently needs AllowAmbiguousTypes to compile in
7.8, but didn't need it in 7.6. It's actually an example of your form of
injectivity C.
The crux is that for list concatenation (like Conal's example of
addition), any two of the inputs/result determines the other
input/result. So it might be useful to have the following.
type family (as :: [Nat]) ++ (bs :: [Nat]) :: [Nat]
| result as -> bs, result bs -> as where
'[] ++ bs = bs
(a ': as) ++ bs = a ': (as ++ bs)
I have serious doubts that GHC could check this injectivity, though.
Fortunately I only use this at concrete enough types that
AllowAmbiguousTypes is sufficient. But really, the types aren't
ambiguous, GHC just doesn't know about the injectivity of (++).
The code below is simplified from code that computes a tensor product of
a tensor with an identity matrix whose size is determined from the
shapes of the input and output tensors.
\begin{code}
{-# LANGUAGE AllowAmbiguousTypes, DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
module Test where
import GHC.TypeLits
type family (as :: [Nat]) ++ (bs :: [Nat]) :: [Nat]
type instance '[] ++ bs = bs
type instance (a ': as) ++ bs = a ': (as ++ bs)
data Tensor (s :: [Nat]) = Tensor -- content elided
-- apparently GHC reduces (++) enough to see that n is determined
leftUnit :: Tensor s -> Tensor ('[n, n] ++ s)
leftUnit Tensor = Tensor
-- accepted in 7.6, not accepted in 7.8 without AllowAmbiguousTypes
rightUnit :: Tensor s -> Tensor (s ++ '[n, n])
rightUnit Tensor = Tensor
-- also accepted without AllowAmbiguousTypes
outsideUnit :: Tensor s -> Tensor ('[n] ++ s ++ '[n])
outsideUnit Tensor = Tensor
useleftUnit :: Tensor '[1,1,2]
useleftUnit = leftUnit Tensor -- type of Tensor is inferred
userightUnit :: Tensor '[1,2,2]
userightUnit = rightUnit (Tensor :: Tensor '[1]) -- type must be provided
\end{code}
On Wed, Sep 17, 2014 at 01:10:13PM +0200, Jan Stolarek 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.
>
> == 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
--
Jason McCarty <jmccarty at sent.com>
More information about the Haskell-Cafe
mailing list