<p>The way Haskell solves this problem is through <em>Type Classes</em> (see <a href="http://homepages.inf.ed.ac.uk/wadler/topics/type-classes.html" rel="nofollow">these papers</a> 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:</p>

<pre><code>class Mappable m where
  map : (a -&gt; b) -&gt; (m a -&gt; m b)
</code></pre>

<p>Then you can instantiate this for arrays (in pseudo-Haskell):</p>

<pre><code>instance Mappable Array where
  map f v = [f(v[i]) | i in (index v)]
</code></pre>

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

<p>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</p>

<pre><code>class Applicative m where
  pure  :: a -&gt; m a
  fusion :: m (a -&gt; b) -&gt; m a -&gt; m b
</code></pre>

<p>and</p>

<pre><code>instance Applicative Array where
  pure x = [x]
  fusion fs v = [fs[i](v[i]) | i in index v]
</code></pre>

<p>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</p>

<pre><code>fusion (map + [1;2;3]) [4;5;6]
</code></pre>

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

<pre><code>+ &lt;$&gt; [1;2;3] &lt;*&gt; [4;5;6]
</code></pre>

<p>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</p>

<pre><code>rem_mod : Int -&gt; Int -&gt; Int
</code></pre>

<p>can be lifted:</p>

<pre><code>rem_mod &lt;$&gt; [1;2;3] &lt;*&gt; [4;5;6] &lt;*&gt; [7;8;9]
</code></pre>

<p>You can find more details <a href="http://en.wikibooks.org/wiki/Haskell/Applicative_Functors" rel="nofollow">here</a>. Finally, I suspect you want to be able to <em>infer</em> 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.</p>

CC BY-SA 3.0
2012-11-12T17:29:04.590Z
2012-11-12T17:29:04.590Z
cody
<p>I am formalizing the type system for a small language, and thus writing inference rules.</p>

<p>Taking <code>unary - operator</code> 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}$.</p>

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

<p>For instance, when I introduce the typing rules for <code>FACT</code> 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?</p>

<p>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}$?</p>

CC BY-SA 3.0
2012-11-12T17:20:36.217Z
Is it enough/ok to state that the Array is functorial, and so for any f : a -> b, map(f) : Array a -> Array b exists ? http://en.wikipedia.org/wiki/Map_%28higher-order_function%29. See for instance http://en.wikibooks.org/wiki/Haskell/The_Functor_class
Romuald
<lo.logic><pl.programming-languages><type-theory><type-systems><type-inference>
How to generalize a map of type for many operators?
SoftTimur
# How to generalize a map of type for many operators?

(Asked by: username_0 on 2012-11-12)

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}$?

**Tags:** lo.logic, pl.programming-languages, type-theory, type-systems, type-inference
> **Comments:**
> **username_1**: Is it enough/ok to state that the Array is functorial, and so for any f : a -> b, map(f) : Array a -> Array b exists ? http://en.wikipedia.org/wiki/Map_%28higher-order_function%29. See for instance http://en.wikibooks.org/wiki/Haskell/The_Functor_class  

---

## 1 answers

### Answer by username_2 on 2012-11-12. Score: 3 | Accepted answer

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.


---

