Improve type signatures

[rpominov]

Based on discussion in #30

Any feedback appreciated :)

[gcanti]

Not sure what these changes add to the spec, there's clearly a pattern

from

<method> :: <type-class> <var> => <signature>

to

<method> :: <type-class> <var> => Type <var> ~> <signature>

so no more info is encoded. The current spec seems clear to me, for example when I consider Semigroup

concat :: Semigroup s => (s, s) → s

that translates to an interface which represents the type class

interface Semigroup<A> {
  concat(x: A, y: A): A
}

and (optionally) to a concat function

function concat<A>(semigroup: Semigroup<A>, x: A, y: A): A {
  return semigroup.concat(x, y)
}

where the first argument represents the type constraint Semigroup s =>.

This translation process can be done mechanically for all the specs.

[rpominov]

This doesn't really add anything new, just clarifies things a bit, and will help to explain parametricity in #30

With current signatures strictly speaking something like this is a correct application of a map method:

List.map(f, Maybe.of(x))

Because only restriction on the second argument is that it's a functor, not necessarily the same functor that type dictionary List represents. With the new signature map :: Functor f => Type f ~> (a → b, f a) → f b we explicitly say that f is the same functor that Type f represents.

[ivenmarquardt]

The only thing that bothers me is this Type or TypeRep or whatever. The semantic of it is only revealed by its name. The following might be a little verbose but also more accurate:

data (String k) => Type k a
map :: Functor f => Type k f ~> (a → b, f a) → f b

data (String k) => Type k a isn't a real data declaration though. At least it is closer to Haskell-style type signatures. Just a thought!

[rpominov]

Not sure I understand. What string are you referring to? Is it "List" in List.map(...)?

[gcanti]

@rpominov I see. Let me explain my point of view though, I hope can be helpful to the discussion. The following signature

map :: Functor f => (a → b, f a) → f b

is not ambiguous because when we write f a we are just representing a data structure parametrised by one type parameter, kind * -> *, (for example Maybe<A> or Array<A> or Promise<A>) not a functor.

From a math point of view a functor F is a pair

F = (mapObject, liftMorhism)

where the first component acts on objects and the second component acts on morphisms. In our case, let's say the category JS, objects are JavaScript types, morphisms are functions and the composition operation of the category is the usual function composition. Hence if we say Array<A> is a functor, strictly speaking, is not correct. When we talk about a functor we must always say how we map objects (types) and how we map morphisms (functions).

The second component of a functor ("lift") has the following signature

lift :: (a → b) → (f a → f b) // <= maps functions to functions

but is commonly implemented as the equivalent

map :: (a → b, f a) → f b

Some examples

1) The functor List = (Array<A>, mapList)

where

• (objects) Array<A> maps a type A to the type Array<A>, i.e the array of elements of type A
• (morphisms) mapList = (f, fa) => fa.map(f)

2) The functor Maybe = (?A, mapMaybe)

where

• (objects) ?A maps the A to the type A | null
• (morphisms) mapMaybe = (f, fa) => fa === null ? null : f(fa)

3) The functor Promise = (Promise<A>, mapPromise)

where

• (objects) Promise<A> maps a type A to the type Promise<A>
• (morphisms) mapPromise = (f, fa) => fa.then(a => f(a))

We can't say Array<A> is a functor, we should say List is a functor.

Coming back to our signature

map :: Functor f => (a → b, f a) → f b

map and f here are tied together because the functor is the pair (f a, map), not f a alone. Hence writing

List.map(f, Maybe.of(x))

doesn't make sense, because you can't mix the map part of a functor (List) with the data structure part of another functor (Maybe).

[ivenmarquardt]

@rpominov No, it should indicate that Type is an Javascript Object or a Map k a, which only accepts a String as key since Symbols are forbidden in static land (AFAIK). But apparently it doesn't make things clearer so it is not worth further talking about it.

[gcanti]

The same argument holds for semigroups, monoids, etc... the type number alone is not a monoid, the triple (number, +, 0) is. In fact you can associate to the same type number several monoid instances, for example (number, *, 1). This is possible in static-land because type classes (better "algebras") are implemented as standalone dictionaries

interface Semigroup<S> {
  concat(x: S, y: S): S;
}

interface Monoid<M> extends Semigroup<M> {
  empty(): M;
}

const sumMonoid: Monoid<number> = {
  empty() { return 0 },
  concat(x, y) { return x + y }
}

const multMonoid: Monoid<number> = {
  empty() { return 1 },
  concat(x, y) { return x * y }
}

but given an instance of a monoid, its empty, concat and carrier set M are tied together and can't be mixed with another monoid instance, by definition

[rpominov]

@gcanti I think I understand what you're saying, and this is a correct way to look at it. I just think there are more than one correct ways to map semantics of our type signatures to semantics of JS implementations of all that. And some of them are easier to grasp. This PR proposes just another hopefully more direct and straightforward way.

The main reason why I want to add this is #30 , where I'm trying to add statement about parametricity to the spec. With this change I'll be able to explain parametricity roughly like this:

In implementation of methods you should only use information about arguments that is known from type signature. You should not inspect them in any way.

For example from this signature map :: Functor f => Type f ~> (a → b, f a) → f b we know that f is a type that dictionary Type f understands, and we're writing map method for the Type f dictionary, so we know everything about f. On the other hand we don't know anything about a and b, and we're not allowed to inspect them.

As another example let's say we're implementing method with this signature mapInner :: (Functor f, Functor g) => Type f ~> (Type g, a → b, f (g a)) → f (g b). There is no such method in the spec we use it only as example. Here we're in the same situation with f, a, and b but what about g? We know that it's a value of a functor and we have it's type dictionary, so the only operation that we can apply to g a is G.map(..). But we don't know anything beyond that, for example what a specific type it's, we know that about f though.

(I still need to write this properly, in a more formal way, and I'm struggling with that to be honest)

So basically having Type f ~> in the signature helps me justify use of low level operations on values of type f a in implementation of map, for example, and explain that this doesn't goes against parametricity. Without Type f ~> I still may be able to justify that the way you did, but it would be just harder to explain.