How to generalize a map of type for many operators?

Question

I am formalizing the type system for a small language, and thus writing inference rules.

Taking unary - operator for example, its entry may be a number as well as an array of number, thus there is an overloading: $-^1$ and $-^a$. Two of their typing rules are $-^1: \text{Integer} \rightarrow \text{Integer}$, and $-^a: \text{Integer Array} \rightarrow \text{Integer Array}$.

Actually there are a lot of operators like unary - operator, which can take one element as well as an array of elements as entry. I just don't know how to generalize this formalization.

For instance, when I introduce the typing rules for FACT operator, one of its rule is $\text{FACT}^1: \text{Integer} \rightarrow \text{Integer}$. I just would like to say $\text{FACT}^a$ exists, and follows "the map of type" logic as $-^a$. Does anyone know how to formalize that elegantly?

Going further for arithmetic binary operators, one rule is $\text{+}^1: \text{Integer} \rightarrow \text{Integer} \rightarrow \text{Integer}$, how could I say $\text{+}^a$ exists, and follows "a map of type" logic, which implies naturally that $\text{+}^a: \text{Integer Array} \rightarrow \text{Integer Array} \rightarrow \text{Integer Array}$?

Answer 1

The way Haskell solves this problem is through Type Classes (see these papers for an overview). The idea is that it is not the $\_^{-1}$ operation that is special; it is the $\mathrm{\bf Array}$ type! To this end, you can define a (statically) overloaded method $map$ which works on each such type. In Haskell:

class Mappable m where
  map : (a -> b) -> (m a -> m b)

Then you can instantiate this for arrays (in pseudo-Haskell):

instance Mappable Array where
  map f v = [f(v[i]) | i in (index v)]

By the way, this class exists and is widely used in Haskell, it goes by the name Functor (and $map$ is $fmap$ for some reason).

This solves the problem for unary operators. For binary operators, or more generally, $n$-ary operators, things get a tiny bit trickier: in this case, you need to figure out what you mean. Do you want the sum of all pairs of numbers in each array, or just the "fusion" of the arrays by the operation sum? I suspect you mean the latter. The way to solve this problem is by another Type Class named $\mathrm{\bf Applicative}$. The definition is

class Applicative m where
  pure  :: a -> m a
  fusion :: m (a -> b) -> m a -> m b

and

instance Applicative Array where
  pure x = [x]
  fusion fs v = [fs[i](v[i]) | i in index v]

The idea is that you can use map to "build up" arrays of partially applied functions, and then use fusion to apply that array of functions to an array of arguments. In the case of $+$ you can just write

fusion (map + [1;2;3]) [4;5;6]

to get what you want. I agree that this is ugly, which is why Haskell has the notation

+ <$> [1;2;3] <*> [4;5;6]

The beauty is that you can iterate this as many times as you want if your function takes more arguments. For example $\mathrm{rem\_mod}$ that computes the remainder of a number $n$ divided by $m$ modulo $r$ of type

rem_mod : Int -> Int -> Int

can be lifted:

rem_mod <$> [1;2;3] <*> [4;5;6] <*> [7;8;9]

You can find more details here. Finally, I suspect you want to be able to infer the places in which to insert the $\mathrm{pure}$, $\mathrm{map}$ and $\mathrm{fusion}$ methods. It may be possible to adapt the type-class resolution mechanism to your purposes, but I don't guarantee you can do this without additional restrictions.