Better type signatures for methods

[rpominov]

While thinking about #32, I've realized that we have another flaw in type signatures that we use. For example:

traverse :: (Traversable t, Applicative f) => Type t ~> (Type f, (a → f b), t a) → f (t b)

Here we say that t must be a Traversable and f must be an Applicative, but that doesn't make sense. We can't require from a type to support an algebra, we can require that only from a module (I use terminology from this comment).

I think we could use something like this instead:

traverse :: (Traversable T t, Applicative A f) => T ~> (A, (a → f b), t a) → f (t b)

which reads as:

• for module T that supports Traversable algebra and works with type t,
• and for module A that supports Applicative algebra and works with type f,
• T has a method traverse,
• that takes module A, a function a → f b, and a value t a,
• and produces f (t b).

---

Somewhat related: #31

[rpominov]

Also maybe we should pull out Traversable T t from the signature, so it would look like this:

Traversable T t
  traverse :: Applicative A f => (A, (a → f b), t a) → f (t b)

which would read like this:

Module T supports Traversable algebra related to type t if:

• T has a method traverse,
• that for module A that supports Applicative algebra related to type f,
• takes module A, a function a → f b, and a value t a,
• and produces f (t b).

I feel like I reinventing type classes though 😄

[tel]

This is kind of what I was talking about in that comment from the PR! Typeclass syntax conflates dictionaries with automated lookup.

To be more concrete, Haskell's compiler translates

traverse :: (Traversable t, Applicative f) => (a → f b, t a) → f (t b)

into

traverse :: (TraversableDict t, ApplicativeDict f) -> (a → f b, t a) → f (t b)

where TraversableDict and ApplicativeDict are "modules" which ascribe to the "Traversable" and "Applicative" signatures/algebras for the specific types t and f. It literally just changes these "constraints" into dictionary/module arguments.

In OCaml you can't quite write this, but the idea would be

traverse : forall a b t f . (TRAVERSE with t = t) -> (APPLICATIVE with f = f) -> (a -> f b, t a) -> f (t b)

where the all caps names reference module signatures which say that whatever dictionary/module gets passed it must satisfy the type TRAVERSE with t = t which you can think of as TRAVERSE t with t as an argument if you like.

[rpominov]

Btw, this starts to look like module signatures, so we won't have that confusion between method signature and module signature if we go this way, because we will have only module signatures.

I think we have 3 options:

• we can kick Haskell's type classes syntax until it works for us,
• or use signatures syntax from OCaml,
• or try to use Flow interfaces syntax, but it probably won't be expressive enough.

I like the first so far, Haskell's syntax seems to be familiar to the largest group of potential readers, and seems like it won't require too many modifications.

[polytypic]

If you are looking for ideas on how to precisely specify the concepts with a module based language, then I'd suggest 1ML. Unlike OCaml, 1ML is expressive enough for the job.

[tel]

I agree @polytypic, 1ML is a good idea. The unification is type theoretically tricky but a good simple model for an untyped language.

[rpominov]

If you are looking for ideas on how to precisely specify the concepts with a module based language

Not sure if I understand what that means :)

As I see it, we need something like OCaml's module signature language. Basically we want to define "algebra" as a module signature + laws. So to my understanding OCaml's signatures are expressive enough for our needs.

Although I don't know anything about 1ML yet, and I just started learning OCaml. Anything in particular I should look at in 1ML if I'll be reading about it?

[rpominov]

A clarification, just in case: whenever I've mentioned "module" before in this issue I've meant dictionary with functions (JS object with functions). Not a ES6 module or anything.

[tel]

The basic idea is that in OCaml the module signature language and module definition language (types and dictionaries) are segregated from the type signature language and the value definition language. This is for technical reasons: the separation helps prevent certain pathological cases with higher-order types which make type foundations difficult and inference impossible.

1ML is a re-envisioning of ML that removes this segregation and lets you see modules as normal dictionaries and module signatures as normal types. It is in that way simpler, but suffers from a more complex type theoretic background and lesser type inference results.

Since the types you're working with are not machine-checked there's a good chance that neither of the above issues will ever be encountered. This make 1ML a pretty good influence.

OTOH, there are a ton of OCaml and even SML resources. There's pretty much a handful of papers alone on 1ML.

[rpominov]

Here is what I came up with. These are signatures for modules. A module to support an algebra will have to match corresponding signature and obey laws. I think this is pretty intuitive for people who're familiar with Flow/TypeScript syntax.

Setoid<T> {
  equals: (T, T) => boolean
}

Semigroup<T> {
  concat: (T, T) => T
}

Monoid<T> extends Semigroup<T> {
  empty: () => T
}

Functor<T> {
  map: (a => b, T<a>) => T<b>
}

Bifunctor<T> extends Functor<T<*, _>> {
  map: (c => d, T<a, c>) => T<a, d>,
  bimap: (a => b, c => d, T<a, c>) => T<b, d>
}

Contravariant<T> {
  contramap: (a => b, T<b>) => T<a>
}

Profunctor extends Functor<T<*, _>> {
  map: (c => d, T<a, c>) => T<a, d>,
  promap: (a => b, c => d, T<b, c>) => T<a, d>
}

Apply<T> extends Functor<T> {
  ap: (T<a => b>, T<a>) => T<b>
}

Applicative<T> extends Apply<T> {
  of: (a) => T<a>
}

Alt<T> extends Functor<T> {
  alt: (T<a>, T<a>) => T<a>
}

Plus<T> extends Alt<T> {
  zero: () => T<a>
}

Alternative<T> extends Applicative<T>, Plus<T> {
}

Chain<T> extends Apply<T> {
  chain: (a => T<b>, T<a>) => T<b>
}

ChainRec<T> extends Chain<T> {
  chainRec: ((a => c, b => c, a) => T<c>, a) => T<b>
}

Monad<T> extends Applicative<T>, Chain<T> {
}

Foldable<T> {
  reduce: ((a, b) => a, a, T<b>) => a
}

Extend<T> {
  extend: (T<a> => b, T<a>) => T<b>
}

Comonad<T> extends Functor<T>, Extend<T> {
  extract: (T<a>) => a
}

Traversable<T> extends Functor<T>, Foldable<T> {
  traverse: (Applicative<U>, a => U<b>, T<a>) => U<T<b>>
}

One tricky part is when an algebra that works with types with two holes extends an algebra that works with types with only one hole. See Bifunctor and Profunctor. I've included map methods in them to show how exactly Functor<T<*, _>> supposed to work. But I expect to have hard time describing this properly.

Also this syntax should allow us to describe algebras that are related to more than one type (see https://github.com/rpominov/static-land/issues/32#issuecomment-258637948) .