16
$\begingroup$

Here, <$> is the infix functor map operation with type Functor f => (a -> b) -> f a -> f b for any functor type, and <*> is the sequential application operator on applicative functors Applicative f => f (a -> b) -> f a -> f b. The function pure, of type Applicative f => a -> f a is the function for bringing values into an applicative functor, similar to return for monads.

A few toy functions to illustrate the question with:

f x = x + 1
g x y = x + y + 1
h z = z ++ z

In a language like Haskell, if we write f [4, 5, 6], we understandably get a type error because the type of f is Num a => a -> a, and Num a => [a] is not a Num a. However, it seems that it would be possible for the compiler/interpreter to notice that Num a => [a] is an applicative functorful of Num as and implicitly rewrite the expression to f <$> [4, 5, 6], which does typecheck, and gives [5, 6, 7].

As more complicated example, if write f [[4, 5, 6], [7, 8], [9]], the compiler/interpreter could notice that Num a => [[a]] is an applicative functorful of applicative functorfuls of Num as and inject two <$>s to rewrite the expression to (f <$>) <$> [[4, 5, 6], [7, 8], [9]], an expression evaluating to [[5, 6, 7], [8, 9], [10]].

You could continue this argument to arbitrarily many functors, and unlike the situation described at the start of my answer here, there's no exponential blowup getting the types to agree since the procedure is to always just unwrap the outermost applicative functor on the argument type until we first find agreement or fail.

(As an aside, the process would have to stop at the first agreement because, taking David Young's example of reverse [[1, 2, 3], [10, 20, 30]] the programmer always has the option to move the function application inward by writing <$> themselves, as in reverse <$> [[1, 2, 3], [10, 20, 30]], but there would be no easy way to go back out a level.)

Similarly, if the compiler/interpreter finds a non-function applied as if a function, it could look for common applicative functors on the outside of both "function" type and the "argument" type and then inject <*>s as needed. For example, g [4, 5, 6] [7, 8, 9] would first become g <$> [4, 5, 6] [7, 8, 9] by the rule above and then g <$> [4, 5, 6] <*> [7, 8, 9] once it turns out that Num a => [a -> a] and Num a => [a] describe functions and compatible arguments inside the same functor. Again, the same trick works on nested functors, though the syntax starts to get fiddly: g [[4, 5, 6], [7, 8], [9]] [[0, 1], [2]] implicitly becomes (<*>) <$> (g <$>) <$> [[4, 5, 6], [7, 8], [9]] <*> [[0, 1], [2]].

On the other hand, here I am deliberately excluding implicit lifting of arguments, which sounds much more dangerous—applying a function to a functorful of values seems like a common intent, whereas applying a functorful of computation to a single value is probably much rarer and better written out explicitly. In particular, an expression like h 7 would still be a type error under this proposal, not rewritten to h (pure 7).

I am also not suggesting that explicit <$>s and <*>s or their equivalents should be dropped from the language—there are other situations where a programmer may want to use them, and, anyway, a developer should always have the option to be explicit if that makes the code clearer.

What are the downsides of implicitly injecting <$> and <*> (but not pure) as described above?

I will enumerate a few obvious ones below, but I am mainly interested in less obvious consequences.

  • Obvious Consequence A: The code is less explicit about the computation being performed. The programmer has to pay especial attention to mismatched types in calls and be aware of the rewrites that are implied.

  • Obvious Consequence B: The implicit rewrite rules are sensitive to the order of currying. An expression like g 4 [7, 8, 9] would be accepted as meaning g 4 <$> [7, 8, 9] because the <$> isn't necessary until the end, whereas the symmetric-appearing g [4, 5, 6] 7 would be rejected because the type-checking rewrite g <$> [4, 5, 6] <*> (pure 7) needs a pure in order to take the 7 last. More dramatically, despite g [4, 5, 6] 7 being rejected, (flip g) 7 [4, 5, 6] would be just fine.

  • Obvious Consequence C: Type inference becomes much more complicated (impossible?), as does reporting type errors in a human-friendly way.

$\endgroup$
7
  • 4
    $\begingroup$ “Type inference becomes more complicated” sounds like a severe understatement to me. I don’t know how you propose to typecheck a program that works this way. After all, your translation appears to assume that all the types are already known, but this isn’t the case. $\endgroup$
    – Alexis King
    Commented Aug 3, 2023 at 22:29
  • 3
    $\begingroup$ What would reverse [[1,2,3],[10,20,30]] evaluate to? $\endgroup$ Commented Aug 3, 2023 at 22:30
  • 4
    $\begingroup$ To me, the most obvious consequence would be that code with a mistake could do the wrong thing instead of giving a type error. $\endgroup$
    – kaya3
    Commented Aug 3, 2023 at 22:36
  • 1
    $\begingroup$ @DavidYoung Clarified in an edit, though your point might still make a good answer because that seems like a likely footgun. $\endgroup$ Commented Aug 3, 2023 at 22:42
  • 2
    $\begingroup$ Here are some syntax-based approaches that can help simplify the use of applicatives and monads: Idris's bang notation and idiom brackets $\endgroup$ Commented Aug 4, 2023 at 0:19

2 Answers 2

19
$\begingroup$

I would like to argue that your proposal is incompatible with Haskell-style ad-hoc polymorphism and global type inference. Doing this with the generality you describe would completely break typechecking.

An example in ordinary Haskell

Consider the simple expression maybeToList (pure ()). How do we typecheck this? Let’s begin by considering the known types involved:

maybeToList :: forall a. Maybe a -> [a]
pure :: forall f a. Applicative f => a -> f a

Both of these functions are polymorphic. To typecheck this expression, we must somehow infer which types to instantiate these polymorphic types at. Conventionally, this is done by generating some fresh solver variables—which I will denote t1, t2, etc.—and then using them to emit a set of constraints:

t1 ~ [t2]
Maybe t2 ~ t3 t4
t4 ~ ()
Applicative t3

Here, Applicative t3 is an ordinary typeclass constraint, while each constraint formed with ~ is an equality constraint that says the types must unify. t1 represents the type of the overall expression, so it’s what we’re solving for.

The first and third constraints are easy to solve: we can just take t1 := [t2] and t4 := (). This simplifies our bag of constraints to this:

Maybe t2 ~ t3 ()
Applicative t3

To solve the remaining equality constraint, we utilize the knowledge that type constructors are unique and injective. This means that $$ ∀f\,g\,a\,b.\: (f\ a = g\ b) ⇔ (f = g) ∧ (a = b). $$ Therefore, we can take t3 := Maybe and t2 := (). This leaves us with simply

Applicative Maybe

left to solve, which we can satisfy using a top-level instance declaration. All constraints are solved, which means the expression is well-typed. To determine what its type is, we recall that we used t1 to represent the type of the whole expression, and t1 = [t2] = [()], the expression’s type is [()].

Attempting this example under your system

If we try to adapt our above reasoning to consider your system, we run into a problem. The issue is that, fundamentally, we cannot emit all these equality constraints! Your proposed system says that the type of a function and the type of its argument do not have to match, so our constraints must be more sophisticated.

To understand the implications of your proposal, it is helpful to pin down the actual typing rule it necessitates. My understanding of your proposal is as a modification to the typing rule for function application. Let’s consider the standard rule for function application first: $$ \begin{array}{l} Γ ⊢ e_1 : \tau_1 → \tau_2 \\ Γ ⊢ e_2 : \tau_1 \\ \hline Γ ⊢ e_1\ e_2 : \tau_2 \end{array} $$ If we just consider automatic introduction of fmap, ignoring automatic introduction of <*> for now, your proposal modifies the typing rule to the following:

$$ \begin{array}{l} Γ ⊢ e_1 : \tau_1 → \tau_2 \\ Γ ⊢ e_2 : \tau_3\ (\tau_4\ (\ldots\ (\tau_n\ \tau_1)\ldots))\\ Γ ⊢ \mathsf{Functor}\ \tau_3\\ \vdots \\ Γ ⊢ \mathsf{Functor}\ \tau_n\\ \hline Γ ⊢ e_1\ e_2 : \tau_3\ (\tau_4\ (\ldots\ (\tau_n\ \tau_2)\ldots)) \end{array} $$

This rule is dramatically more complicated. The sequence of type constructors $\tau_3$ through $\tau_n$ can vary arbitrarily in length, and it may even be empty. To think about how we might encode this in a Haskell-like type system, we can consider an encoding into modern GHC Haskell that uses a type family to represent the nested sequence of type constructor applications:

type family Apps :: [Type -> Type] -> Type -> Type where
  Apps '[]       a = a
  Apps (f ': fs) a = f (Apps fs a)

type family All :: (k -> Constraint) -> [k] -> Constraint where
  All _ '[]       = ()
  All c (a ': as) = (c a, All c as)

This type family allows us to encode $\tau_3\ (\tau_4\ (\ldots\ (\tau_n\ \tau_1)\ldots))$ as Apps '[τ₃, τ₄, ..., τₙ] τ₁, and it allows us to encode the need for each of those types to belong to Functor as All Functor '[τ₃, τ₄, ..., τₙ]. This is helpful, since it allows us to adapt the equality constraints we generated above to handle your proposed system:

t1 ~ Apps t5 [t2]
Apps t5 (Maybe t2) ~ t3 t4
t4 ~ ()
Applicative t3
All Functor t5

Here, t5 :: [Type -> Type], and it represents the as-yet-unknown list of functorial type constructors that maybeToList might need to be automatically lifted over. Note that I am ignoring the additional use of Apps that would technically also have to be introduced by the use of pure, but that would make this example even more complicated, and your rules suggest that it could be immediately eliminated, so I am omitting it for the sake of simplicity.

Let us consider how we might approach solving this bag of constraints. As before, we can start by immediately solving t1 and t4 by taking t1 := Apps t5 [t2] and t4 := (). This leaves us with the following constraints:

Apps t5 (Maybe t2) ~ t3 ()
Applicative t3
All Functor t5

How do we proceed? It’s worth noting that, under GHC’s current typechecking rules for type families, we actually can’t. The root problem is that Apps is not injective: Apps '[] (F A) and Apps '[F] A both reduce to F A. This makes it very challenging to extract information from this constraint.

Of course, since we’re planning to wire this functionality into the type system, we are not limited to doing whatever GHC’s type family solver happens to do. One way we could make this constraint solvable would be to perform what is known in the literature as improvement. Improvement is a process by which the constraint solver can identify unifications that must hold in order for a given constraint to be able to be solved, and with luck, those unifications may turn an unsolvable constraint into a solvable one.

In this particular case, we can convince ourselves that the only valid solution for this constraint is if t5 = '[]. We can make this argument by considering that t3 () is always going to be precisely one type constructor applied to a concrete type, and Apps t5 (Maybe t2) requires at least one type constructor due to the use of Maybe. Therefore, if t5 were ever a non-empty list, the types could not possibly unify, and we can take the improvement t5 := '[]. This allows both Apps and All to reduce, and we’re left with the constraints from before:

Maybe t2 ~ t3 ()
Applicative t3

These can solve the same way they did before, and we can accept this expression.

Improvement is sometimes impossible

The complexity involved in the above example is already pretty bad. However, it gets worse: the improvement rule we used does not apply in general, and when it doesn’t, it’s not even clear how to proceed.

Consider the slightly different expression maybeToList (pure mempty). Under ordinary Haskell, this modified expression has the perfectly natural type Monoid a => [a], but under your proposed system, its type is much less clear. It leaves us with the following bag of constraints:

t1 ~ Apps t5 [t2]
Apps t5 (Maybe t2) ~ t3 t4
t4 ~ t6
Applicative t3
Monoid t6
All Functor t5

After taking t4 := t6, we’re left with the highly unhelpful constraint Apps t5 (Maybe t2) ~ t3 t6, and unfortunately, this constraint is not improvable, as there are infinitely many potential solutions:

  • We could take t5 := '[] as before, in which case t3 = Maybe and t4 = t2.

  • We could also take t5 := '[t7], in which case t3 = t7 and t4 = Maybe t2.

  • In fact, since t4 could contain any number of applications of some type constructor, t5 could be of any length at all.

It may seem as though this means we’ve lost principal types in our system, but this is not necessarily true. This expression does have a principal type, it is just quite the mouthful:

forall f fs a. (Applicative f, All Functor fs, Monoid (Apps fs a)) => Apps (f ': fs) [a]

However, not only is this type somewhat terrifying, it’s also incredibly ambiguous in the sense that Haskell uses the term: since Apps is not injective, knowing the expected result type at the site that this expression is used may not necessarily be enough to determine f, fs, and a. Moreover, even though this principal type exists, it’s not clear to me that an algorithm exists to reliably infer this type given only the original expression. Perhaps there is some way to do it, but I don’t know what it is.

What if we abandon global type inference?

Suppose we give up on global type inference. Certainly, if we abandon type inference altogether and demand that the user write all type annotations explicitly, we can implement your scheme, but this means explicitly instantiating every polymorphic value, which I think would be considered a non-starter even for languages with exceptionally austere type inference schemes.

A compromise would be to use some form of local type inference, which sounds potentially promising. However, it’s worth pointing out that a local type inference scheme would require a significant number of additional type annotations for polymorphic code, and abstractions like applicative functors generally necessitate lots of polymorphic code, so the cure may very well end up being worse than the disease. Nevertheless, you certainly could come up with some ad-hoc scheme that would support relatively simple type inference. However, you’re still quite limited in what you can achieve.

The way your proposal works makes a distinction between lifting a function and lifting an argument. This means that the argument’s type must be determined largely independently from the function’s type! This is a major problem since functions like pure are polymorphic in their return types, and the maybeToList (pure ()) example illustrates how this is likely to cause trouble. In such an expression, the type of the argument is determined from its context, but this simply cannot be done in general if every function can be lifted.

You would therefore need to either explicitly annotate this expression and all expressions like it, or you’d need to develop some sort of ad-hoc bidirectional type system that allows propagating expected type information in a sufficiently limited way. Could you design such a thing? Maybe! But it’s not immediately clear to me that it would be usable, so I’m not convinced that local type inference is an easy way out.

$\endgroup$
9
  • $\begingroup$ Forgive me if I'm missing something, and forgive me that this concern is hard to format in a comment, but doesn't this definition of <: treat <$> as having type (Functor f, Functor g) => (a -> b) -> f a -> g b instead of Functor f => (a -> b) -> f a -> f b, and that's the real source of the problem in your example? [contd.] $\endgroup$ Commented Aug 4, 2023 at 2:26
  • $\begingroup$ If we insist that the functors wrapped around a function's result agree with those unwrapped from its argument, then instead we get the system t1 ~ t5… [t2] ∧ t5… Maybe t2 ~ t6… t3 t4 ∧ t6… t4 ~ () ∧ Applicative t3 where t5… and t6… both represent (possibly empty) sequences of functors, and that system does have a unique solution t1 = [()] ∧ t2 = () ∧ t3 = Maybe ∧ t4 = () ∧ t5… = {no functors} ∧ t6… = {no functors}. (It might still be the case that type inference breaks on some other example, though.) $\endgroup$ Commented Aug 4, 2023 at 2:27
  • $\begingroup$ @Wheelwright You’re right that I made a small mistake in failing to adequately account for the consistency in the result. I do think you’re right that you could extend the “subsumption” relation to be indexed by a list of type constructors of kind Type -> Type, but this significantly complicates the type system, as now you are dealing with type-level lists. If you want to retain principal types, those lists must somehow be manifested in the source language, and standard Haskell certainly does not support that. $\endgroup$
    – Alexis King
    Commented Aug 4, 2023 at 3:19
  • $\begingroup$ @Wheelwright Moreover, we can easily make the example definitively fail to typecheck by wrapping the expression in show, since show requires the type of its argument to be unambiguous. Perhaps you could introduce some special defaulting scheme for these type-level lists, much as Num is defaulted to Integer, but this is already growing quite complex. $\endgroup$
    – Alexis King
    Commented Aug 4, 2023 at 3:22
  • $\begingroup$ Regarding the latest edit, I don't think we can soundly say a priori that t3 t4 <: Maybe t2 because the result of pure might be wrapped in functors (the t6… in my t5… Maybe t2 ~ t6… t3 t4). We would have to first unify t4 with () to know that there are none there. $\endgroup$ Commented Aug 4, 2023 at 17:26
-3
$\begingroup$

My experience in functional programming is actually limited. Tell me if I misunderstand anything. What you have described is sometimes called vectorization (unhelpful link), or array programming (unhelpful term, but Wikipedia calls it this). I'm assuming you are asking about vectorization in general, not limited to functional programming language.

I don't think it has big downsides, as it is already done in many languages, if we don't restrict it to functional programming languages. But it may need to be designed carefully, to avoid pitfalls.

Mixing of dimensions

if x is [a, b, c] and y is [d, e, f], x + y actually has two different intuitive meaning. One is to add corresponding elements, the other is to add all pairs as in a Cartesian product. The later also has an implementation detail that whether the result is one dimension or two dimensions.

If you choose corresponding elements, where the term vectorization is most appropriate, people may expect if a + y and b + y are valid, [a, b] + y is automatically always valid and always means the previous two combined into an array. But it is not true. If y is actually [d, e, f], [a, b] + [d, e, f] would be an vectorized operation on lists with unequal sizes, which may not make much sense, or at least doesn't give the expected result.

If you choose all pairs, as defined in the question, I was once in that situation, before knowing APL I think, in a procedural programming language, not even objective oriented. In that language, parameters are always passed by references, so every parameter is both an input and an output of the function. Problem arises when you call multiple functions with the same parameters in a sequence:

var1 = input
var2 = var3 = 0
func1(var1, var2, var3)
func2(var1, var2, var3)
func3(var1, var2, var3)

Think about expanding another function calling the three functions to its internal content. The later functions are supposed to use the previous function's one set of consistent output as the input, but it actually gets the Cartesian product of all parameters across different sets of data. This is especially a problem if you don't want to restrict the parameter types in most functions, where wrapping them into a function would still be equivalent to them, and there won't be an easy way to get the desired semantic.

It's much more hidden in a functional programming language, where multiple return values are not in the basic syntax. You may get some problems once you wanted to split multiple return values. And you may have different problems if you use different ways to split them and use them.

But a simple possibility would be someone defines a function without specifying the parameter must be non-array, and use its parameter two times in the function, and someone calls it on an array. These two functions would be very different if the type of x is not specified:

f x = x + x
g x = 2 * x

Strings

In many languages, strings work like arrays of characters. But they are often logically like simple values that should not be vectorized into while you are vectorizing a list of them. The inherited properties of arrays would become a trouble. A common use case is to do vectorized concatenation. Someone may expect ["a", "b"] ++ ["c", "d"] to work, but it obviously doesn't because the operator ++ already had a meaning in this case, which is array concatenation. You may make strings and character arrays different, and define different operators for them. But the programmers need to remember more things, and there might be another case that also use arrays as simple values.

If the language supports operator overloading, programmers should also be careful not to overload the array operations, so that they won't make the operator unable to be vectorized. If you provide some nice operators such as union and intersection, that means the overloadable options are fewer. Worse if you ever add predefined overloading to already overloadable operators.

The solution in APL

In APL, arrays could be "enclosed" to make it like a simple value, called a scalar value. Vectorized operations are on corresponding scalar elements, and could be vectorized recursively for the basic operations that are inherently vectorized. Non-vectorized functions could be non-recusively vectorized to the level of scalar values using an operator, just like using your implicit modifications explicitly. But arrays could have multiple dimensions above the scalars, without enclosing, different from nested enclosed arrays. So you could still take advantage of vectorization to work with strings, for not needing to specify the number of levels, and not needing to write that operator many times, by making strings enclosed scalars in a bigger array of any number of dimensions. You could also specify the dimension while using many functions, and there is an operator for outer product, to help dealing with dimension problems.

There are built-in functions (used like operators in other languages, but "operators" in APL refer to high order functions) to enclose a dimension, and "disclose" to extract from scalar values to make a new dimension, to convert between the two formats. You may think multi-dimensional arrays doesn't conflict with the concept of functors, but it requires slightly more thinking to allow moving a dimension in and out, as a basic feature to support this semantic better.

Vectorization is basically a possible property of a function. User defined functions are not by default vectorized, mostly because parameter types are not usually specified, so the interpreter wouldn't know if your function already makes sense directly on arrays. But many user defined functions could appear as vectorized, because you call vectorized functions for simple calculations in its implementation.

I repeat that my answer only says it may need to be designed carefully. So APL might not be removing all the above listed situations. In some cases it instead defined more things to work with the listed situations, to supplement the implicit injection.

$\endgroup$
12
  • 1
    $\begingroup$ It's not clear in this how it applies to any functor other than list (or ZipList); what is the equivalent translation to e.g. the Maybe or function Functors, or even something like Product? $\endgroup$
    – Michael Homer
    Commented Aug 4, 2023 at 2:14
  • $\begingroup$ I'm a little torn on how to vote on this. Like mentioned above, the question is about all applicative functors; lists were just an example. The discussion on mixing of dimensions is a good answer, but to a different question, since here those decisions were already all made by how the type was defined as an instance of Applicative. The other parts get at possible ambiguity about what "level" a reader will think the function applies at, like in the reverse [[1, 2, 3], [10, 20, 30]] example, and that's an on-topic concern, so maybe refocus the answer on that idea? $\endgroup$ Commented Aug 4, 2023 at 2:28
  • 5
    $\begingroup$ I don’t think this answers the question. $\endgroup$
    – Alexis King
    Commented Aug 4, 2023 at 3:10
  • 1
    $\begingroup$ What you call "vectorized operations" and APL calls "scalar functions" don't really work how you explain they do, scalar functions do go through boxes, but after they have been interpreted as scalars. The section could probably be written more clearly, it seems to imply that 1 2 3+⊂4 5 6 wouldn't work, or that's what I understand it to mean. Also, in the context of APL, where "function" and "operator" mean vastly different things, I wouldn't use them interchangeably. $\endgroup$
    – RubenVerg
    Commented Aug 4, 2023 at 9:28
  • 2
    $\begingroup$ This answer does not answer the question. It is perhaps an interesting answer to an entirely different question. But it really does not answer this question in any capacity. It is somewhat remarkable to me that it has currently attracted 4 upvotes in spite of this fact. $\endgroup$
    – Alexis King
    Commented Aug 4, 2023 at 15:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .