## Looking for an auto-lifting language.

I have been looking for a language that includes the following form of resolution, but have not yet come to one.

Given a function f: a -> b, and a list l: [a], I would like for the language to consider "f l" a valid expression. In particular, I would like it to automatically "lift" f to be typed as f:[a] -> [b] by rewriting "f l" as "map f l". In general, given a functor F : a -> F a, a function f : a -> b, and value v : F a, I would like for the expression "f v" to be rewritten as "F(f) v : F(b)".

In addition, a multivariable method such as + : double -> double -> double, would lift based on the types of its arguments. Examples:
x, y: Id double |- (x + y) : Id double
x, y: [double] |- (x + y) : [double]
x, y: Interval double |- (x + y) : Interval double
x, y: Dist double |- (x + y) : Dist double
x: Dist double, y: Id double |- (x + y): Dist double
etc...

I understand that all of this can be done by augmenting the code to be written in terms of do notation (almost, these are just plain functors, not monads), but I want a language that does that for me: do x < - a, y <-b, return $x + y (is equivalent to) a + b. If such a language doesn't exist, can I get suggestions on best/easiest ways to accomplish this. I have considered using a preprocessor/modifying the type resolution process to include the additional code generation for an existing language, but I am not sure if there are other options/which is better. I wrote the above in Haskell notation just for communication purposes. OO languages would be appreciated as well. Many thanks, Rob ## Comment viewing options ### APL does this The domain of APL values is multidimensional arrays, where scalars can be identified with arrays of rank 0. Most operators are automatically lifted to work on arrays of any rank; binary operators require both operands to have the same shape, except that a scalar operand will be cast to the same shape as the other operand if necessary. ("Rank" = number of dimensions; "shape" = sequence of maximum indices for the dimensions.) ### Previously on LtU There was a good discussion of automatic lifting in APL in this previous discussion. ### Excellent, this behavior is Excellent, this behavior is spot on with what I was looking for, at least in the domain of operations on multidimensional arrays. I will investigate this further. I did various searches on APL, and I see that most of its variants are dynamically typed as well. Are you aware of an off-shoot that is statically typed? Also, perhaps there is one that have built-in constructs for creating data structures: e.g. named records/classes, etc. I didn't see any referenced. Much appreciated. ### J If you are really interested in lifting in the domain of arrays, I suggest that you study J rather than APL. J is the successor of APL, cleaning-up and advancing many of its concepts. There is a huge, up-to-date literature on J, and freely available implementations to play with and learn from. In J, the central concept that one needs to know with respect to â€˜liftingâ€™ is rank, but there are a number of related and also important concepts: axis, shape, frame, cell, item, tally, verb rankâ€¦. The official J reference is the Dictionary (see esp. Chapter 20 â€˜Rankâ€™), but it is not suitable for a beginner. I'd suggest reading the following instead: • the J Primer â€“ Part 5, titles â€˜Atomâ€™, â€˜Listâ€™, â€˜Tableâ€™, etc; • this article; • Roger Hui's â€˜Rankâ€™ essays 1 and 2. Now, J is also, like APL, dynamically typed. There are several substantial reasons for that, but think of it this way: in J, ranks play a similar role to that of types in, say, languages with algebraic type systems. In Haskell, types control how things interact; in J, it is ranks. And as value ranks are necessarily dynamic, the very concept of static â€˜typingâ€™ does not make much sense in J. ### Wonderful, going to work Wonderful, going to work through these. I see what you are saying about the typing. I will try to see types the J way. ### Lifting can be done in more than one way The problem with automatic lifting is that lifting can be done in more than one way for one functor. For example, [1,2] + [10,20] using the list monad yields [11,21,12,22], and in APL it yields [11,22]. Another sensible answer would be [[11,21],[12,22]]. Also, if you want to lift f: a -> b to f:[a] -> [b], and then apply this to (+) then it becomes [Double] -> [Double -> Double]. ### The previous discussion The previous discussion James posted (excellent, thank you) brings up this issue. I'm not sure that I follow why this is a show stopper. My plan, which is why the suggestion of APL threw me off a bit :), was to rely on the type to dictate how, e.g., your above examples would behave. Indeed, I see now that a functor alone isn't sufficient, but perhaps an additional operation * : F(a->b)->F(a)->F(b) (applicative functor?) would do the trick. In particular, it is clear that f: a->b should map to f:[a]->[b] via the map function in either APL or Haskell examples, i.e (+) [1,2] : [Double->Double]. The question lies as to how ((+) [1,2]) [10,20] should behave. i.e. how should we evaluate [Double -> Double][Double]. To be faithful to Haskell, this would lift to: do f <- (+)[1,2]; x <- [10,20]; return$ f x. But we could just as easily lift it to: map (\(f,x) ->f x) \$ zip ((+)[1,2]) [10,20].

In general, given F(a->b) F(a) we get a choice as to how to evaluate, and we can do so by transforming F(a->b)F(a) to (*)(F(a->b)) F(a). If the list functor were to be augmented with the above * operation (call it Zip for APL behavior/and Cart for Haskell behavior), then we would be able to differentiate:
x : Zip a, y : Zip b, f : a -> b -> c |- f x y : Zip c
x : Cart a, y : Cart b, f : a -> b -> c |- f x y : Cart c
x : [a], y : [b], f : a -> b-> c |- f x y : (unable to resolve)

Is this the source of the "ambiguity" problem, or is there something I am missing?

### Applicative functors

You might be spot on with applicative functors. See f.e.