Enforce parametricity

[rpominov]

@davidchambers @joneshf Could you take a look? I'm not sure about wording terminology and such.

Related: fantasyland/fantasy-land#184

[davidchambers]

Another option is to include explicit foralls as PureScript does. For example:

map :: forall f a b. (Functor f) => f a ~> (a -> b) -> f b

[rpominov]

Good idea, although type signatures will become a bit noisier.

There is another unrelated issue with type signatures, btw. Restrictions like Functor f are not restrictive enough. For example something like this is correct according to type signature List.map(f, Maybe.of(1)) because signature says for any functor f give me a f a as second argument.

[rpominov]

Just noticed that you've included f into forall f a b. In this case I'm not sure how forall will help with statement about parametricity that I'm trying to add. I was thinking we could mention only a and b in foralland then say that unrestricted type variables are variables in forall, but if f also there that won't work.

[ivenmarquardt]

There is another unrelated issue with type signatures, btw. Restrictions like Functor f are not restrictive enough. For example something like this is correct according to type signature List.map(f, Maybe.of(1)) because signature says for any functor f give me a f a as second argument.

Maybe I'm missing the point but map :: Functor f => (a -> b, f a) -> f b is the type signature of map of the Functor typeclass. For the List instance it would be: map :: (a -> b, [a]) -> [b]. You can't apply map's general type signature to specific Functor implementations.

[rpominov]

@ivenmarquardt Yeah, you're probably right here.

I've just was trying to explain parametricity better based on type signature, and say something like "a and b are unrestricted, but we know that f is a Functor so we can use it as a Functor", but in fact when it comes to implementation we don't only know that f is a Functor, but also know what a specific type it is, like List, so we can do even more with it...

So it all comes down to explaining parametricity in the spec again.

[ivenmarquardt]

Hm, actually I was wrong, sorry. map :: Functor f => (a -> b, f a) -> f b already indicates that the context must be preserved. List.map(f, Maybe.of(1)) doesn't match the type signature, because f (of the type signature) must be the same Functor.

[rpominov]

I think it's confusing because we're trying to use syntax designed for Haskell in JS. In Haskell signature fmap :: Functor f => (a -> b) -> f a -> f b makes sense because there is actually a function fmap that can be applied to any functor, and under the hood behaviour is dispatched to specific Functor implementation based on types.

But in static-land we can't have such "global" map function, instead we only have List.map, Maybe.map etc. So there is a mismatch in language's constructs that is confusing.

[joneshf]

fmap allows the programmer to implicitly ignore the Functor f argument, but the compiler still has to find the Functor f at some point. Which means that if you monomorphize it to a specific Functor like List, it has to grab that function from somewhere. It's effectively fmap :: Functor f -> (a -> b) -> f a -> f b–if you like in uncurried fashion fmap :: (Functor f, a -> b, f a) -> f b. What we do in FL is equivalent to map :: f a -> (a -> b) -> f b. Though it's defined on the object in js. What you do in SL is explicitly map :: (a -> b, f a) -> f b. But, there's no universal fmap in either language that works for all things magically without knowing what those things are first. There are syntactic differences, but under the hood they work effectively the same; in other words, you CAN have a "global" map function.

N.B. You can probably skip this next part, but I want to set up some context.

I think there's an important difference between the function being defined and the function being implemented. I'm going to talk abstractly about it, because there are too many details to flesh out here.

This syntax:

class Functor f where
    fmap :: (a -> b) -> f a -> f b

defines a function with the actual type Functor f => (a -> b) -> f a -> f b. This is the ONLY function you actually use in Haskell when you write fmap. You can monomorphize it if you want to use it in a more specific case, like mapInt :: Functor f => (Int -> Int) -> f Int -> f Int, mapList :: (a -> b) -> List a -> List b, or mapShow :: (Functor f, Show a) => f a -> f String, but you are always using this one function.

This syntax:

instance Functor List where
    fmap = undefined

provides an implementation of fmap for List. The programmer NEVER uses this function. They don't even have access to it. It's entirely written for the compiler to do its dirty work. If you type fmap show [1,2,3], the function you put in there is the one defined in the class.

On to my point

In FL, we only spec out the class part, but we don't provide any of the functions you would actually use. When you go to implement Functor for List in js, you're providing something similar to the instance part. However, since js doesn't have type class machinery, the implementation you just wrote is then used as if it were a monomorphized version of the class version of fmap. You're writing the instance bits, and then doing all the work the compiler does in Haskell. It's more explicit in SL, because you move from methods on an object to functions that use an object.

We have to do all the dirty work that the compiler does, but we also changed the signatures around when converting. The simplest move is to make the signatures more accurate. SL could provide functions with more accurate signatures:

// map :: Functor f -> (a -> b, f a) -> f b
function map(functor) {
  return functor.map;
}

There's your "global" map function! It's not the most ideal thing, since you have to know your Functor ahead of time. One trick you can do is move the Functor f to the last argument, and rely on functions to clean up "some" of it. It's sort of like CPS...

Could we implement something more similar to type classes in js? Probably. I think @CrossEye has tossed around the idea a few times. Maybe somebody should attempt to do that. But we currently don't, so we end up where we're conflating both the class stuff and the instance stuff. That lets us (forces us to?) pass around instance stuff, when we really don't want to.

The point, though, is that it doesn't have to be!

[rpominov]

Thanks @joneshf , you've put my mind in order :)

you CAN have a "global" map function

Yea, I probably shouldn't say that it's impossible. Still nobody came up with a good way of doing it in JS as far as I know. There is some discussion even in this repo #3 , and I like your idea of providing concrete type at the end, need to think more about it.

fmap :: (Functor f, a -> b, f a) -> f b

Small remark: If I understand correctly Functor f here represents a type dictionary. I currently use capital letters for type dictionaries as described here. Although I like better @davidchambers 's idea to use TypeRep f, will probably switch to that soon.

Translating this to function call it would look like fmap(List, f, [1, 2]) which is not far from List.map(f, [1, 2]) and we usually use ~> in type signatures in place of ., so translating back to types it's map :: Functor f => TypeRep f ~> (a -> b, f a) -> f b — probably that's how type signatures should look like in this spec!

[dead-claudia]

@rpominov

@isiahmeadows Yeah, you're probably right here.

Could you point me to what you're talking about? I'm missing context.

[rpominov]

@isiahmeadows This was a response to #30 (comment)

Edit: ah, sorry, I've meant to mention @ivenmarquardt there.

[davidchambers]

There is another unrelated issue with type signatures, btw. Restrictions like Functor f are not restrictive enough. For example something like this is correct according to type signature List.map(f, Maybe.of(1)) because signature says for any functor f give me a f a as second argument.

We must replace all occurrences of f in the same manner. For example:

map :: forall f a b. (Functor f) => f a ~> (a -> b) -> f b

-- replace `(Functor f) => f` with `List`
List$prototype$map :: forall a b. List a ~> (a -> b) -> List b

f is constrained just as a and b are. f is additionally constrained by Functor f.

Just noticed that you've included f into forall f a b. In this case I'm not sure how forall will help with statement about parametricity that I'm trying to add. I was thinking we could mention only a and b in foralland then say that unrestricted type variables are variables in forall, but if f also there that won't work.

I followed the form of the ap example from the Explicit forall section of the PureScript wiki:

ap :: forall m a b. (Monad m) => m (a -> b) -> m a -> m b

I believe the idea is that all type variables are introduced (m, a, and b in this case), then constrained (m must be a member of the Monad type class in this case).

you CAN have a "global" map function

Yea, I probably shouldn't say that it's impossible. Still nobody came up with a good way of doing it in JS as far as I know.

Is Z.map unsatisfactory in some way?

Although I like better @davidchambers 's idea to use TypeRep f, will probably switch to that soon.

Full credit should go to @tel for this idea. :)

[rpominov]

List$prototype$map :: forall a b. List a ~> (a -> b) -> List b

Yea, but we can't use concrete types in the spec. Something like the following looks good to me though:

map :: Functor f => TypeRep f ~> (a -> b, f a) -> f b

Also prototype confuses me, seems like you're thinking about fantasy-land.

I followed the form of the ap example from the Explicit forall section of the PureScript wiki:

Right and this is most likely correct, but I just don't see how forall will help with the statement about parametricity that I'm trying to compose in this PR.

Is Z.map unsatisfactory in some way?

Yea, for fantasy-land this is easier, I meant for static-land.

[davidchambers]

Clearly I've been thinking a lot about Fantasy Land recently. 🌈

I'm sorry for making an unhelpful comment.

[ivenmarquardt]

I like it:

map :: Functor f => TypeRep f    ~>  (a -> b, f        a ) -> f b
                            List .map(f,      Maybe.of(x)) // doesn't match
                            Maybe.map(f,      Maybe.of(x)) // does match
                            List .map(f,      List.of (x)) // does match

I wonder what the advantage of forall is. What additional information does it provide?

[dead-claudia]

Translating this to function call it would look like fmap(List, f, [1, 2]) which is not far from List.map(f, [1, 2]) and we usually use ~> in type signatures in place of ., so translating back to types it's map :: Functor f => TypeRep f ~> (a -> b, f a) -> f b — probably that's how type signatures should look like in this spec!

I like how this could look (although IMHO I feel it's a bit awkward). Here's a quick summary of the existing types using that idea (I've changed TypeRep f to Type f to match the current spec):

equals   :: Setoid s      => Type s ~> (s, s) -> Boolean
concat   :: Semigroup s   => Type s ~> (s, s) -> s
empty    :: Monoid m      => Type m ~> () -> m
map      :: Functor f     => Type f ~> (a -> b, f a) -> f b
bimap    :: Bifunctor f   => Type f ~> (a -> b, c -> d, f a c) -> f b d
promap   :: Profunctor f  => Type f ~> (a -> b, c -> d, f b c) -> f a d
ap       :: Apply f       => Type f ~> (f (a -> b), f a) -> f b
of       :: Applicative f => Type f ~> a -> f a
chain    :: Chain m       => Type m ~> (a -> m b, m a) → m b
chainRec :: ChainRec m    => Type m ~> ((a -> c, b -> c, a) -> m c, a) -> m b
reduce   :: Foldable f    => Type f ~> ((a, b) -> a, a, f b) -> a
extend   :: Extend e      => Type e ~> (e a -> b, e a) -> e b
extract  :: Comonad c     => Type c ~> c a -> a
traverse :: (Traversable t, Applicative f) => Type t ~> (Type f, (a -> f b), t a) -> f (t b)

[dead-claudia]

I almost feel that either Haskell's class ... where syntax (to avoid confusion, I'd recommend type ... where), OCaml's module type ... = sig ... end, or a variant thereof, could help make this more readable and clearer, since Static Land types are very similar to OCaml modules.

[dead-claudia]

@ivenmarquardt

I wonder what the advantage of forall is. What additional information does it provide?

Probably not much - that usage is already implicit in Haskell IIRC.

[rpominov]

I almost feel that either Haskell's class ... where syntax (to avoid confusion, I'd recommend type ... where), OCaml's module type ... = sig ... end, or a variant thereof, could help make this more readable and clearer, since Static Land types are very similar to OCaml modules.

This looks interesting, @isiahmeadows . Could you provide some examples of how this could look like?

I've opened a PR about signatures #31 , let's move this discussion there.

[rpominov]

I've updated parametricity explanation and would appreciate any feedback!

[joneshf]

It might be helpful to mention why violating parametricity is bad. Namely because it'll break something

[rpominov]

Like Functor's composition law? Sounds like a good idea, but one may think "why have parametricity requirement then if we already have corresponding laws?".

As far as I understand parametricity actually gives composition law for free, and I'm guessing that it gives more than that. So the value of this requirement is to have that extra value that parametricity gives besides laws that we already have anyway.

[joneshf]

Sure. But, this example sometimes breaks the identity law.

> X.map(x => x, {x: false})
{ x: false }
> X.map(x => x, {x: {}})
{ x: {} }
> X.map(x => x, {x: "wat"})
{ x: 'wat' }
> X.map(x => x, {x: {hello: "world"}})
{ x: { hello: 'world' } }
> X.map(x => x, {x: new Date()})
{ x: 2016-10-24T14:45:47.112Z }
> X.map(x => x, {x: 1})
{ x: 2 }
> X.map(x => x, {x: [1,2,3]})
{ x: [] }

Might need a more complex example to show where it breaks something more spectacularly. Like the Maybe data type that people usually start with, which checks null and whatnot.

[rpominov]

It's hard to came up with a good example. I have the following so far, it still seems contrived, and grew too big for a spec to my taste.

---

Here is another example of a Maybe type that violates parametricity requirement:

Maybe.Nothing = {type: 'Nothing'}
Maybe.Just = x => {type: 'Just', value: x}
Maybe.map = (f, v) => {
  if (v.type === 'Nothing') {
    return v
  }

  const a = v.value
  const b = f(a)

  if (b === undefined) {
    return Maybe.Nothing
  }

  return Maybe.Just(b)
}

We make implicit conversion of undefined to Nothing.
This looks convenient because we can now do safer operations with arrays for example:

const first = arr => arr[0]
const inc = n => n + 1

inc(first([])) // NaN

Maybe.map(inc, Maybe.map(first, Maybe.Just([]))) // Nothing

But what if undefined is a ligitimate value for us:

const first = arr => arr[0]
const isUndefined = x => x === undefined

Maybe.map(isUndefined, Maybe.map(first, Maybe.Just([undefined]))) // Nothing, but we expect Just(true) 

[rpominov]

Also the less contrived I'm trying to make it the bigger it grows :)

I think the purpose of example here should be not to explain why we require parametricity, but rather to explain what exactly we require. Answers to why questions are very important but should not live in a specification, imo.

So maybe current example is good enough, or we could switch to a Maybe example but leave only first code snippet, with an additional code comment:

  if (b === undefined) { // this is not allowed
    return Maybe.Nothing
  }

[tel]

Here's a common example of a parametricity violation (and the havoc it causes)

// Assume `goodMap : (a -> b, Maybe a) -> Maybe b`

// Same type, but devious!
// badMap : (a -> b, Maybe a) -> Maybe b
function badMap(f, m) {
  if (m.value == 0) {
    return Maybe.Nothing
  } else {
    return goodMap(f, m)
  }
}

This is obviously cheating—it relies on (heterogenous) equality being defined for all values in Javascript—but nothing about the bare type variable a reflects that idea. If parametricity holds then we know certain so-called "free theorems" about the behavior of badMap, but since we've violated parametricity those will not hold.

Here's the free laws we can expect: http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi where you type in (a -> b) -> (Maybe a -> Maybe b) and click "hide type instantiations" and then look at the bottom where "Reducing all permissable relation variables to functions" has happened

-- our function is named `f`
(forall x . h (p x) = q (g x)) ==> forall x . fmap h (f p x) = f q (fmap g y) -- or
h . p = q . g ==> fmap h . f p = f q . fmap g

or, any such function should commute with fmap so long as the lifted functions commute as well. Let h = p = q = g and we'll see that any such function should commute with fmap generally.

fmap g . f g = f g . fmap g

This obvious is violated by badmap since it has special behavior which blows up on hitting a particular value and that blow-up won't commute.

[tel]

I honestly think that while the concept of parametricity and higher order generalization are super wonderful, that Haskell's typeclasses as the mechanism for popularizing these ideas are harmful.

Typeclasses combine (1) higher order abstraction and (2) implicit search together into an incredibly usable language facility that Haskell and basically no other language has. The important thing to steal is (1), not (2).

So, I'd really recommend taking more points from OCaml/SML here. The thing that static-land calls a "type" is what OCaml calls a module. The fact that it's abstracting over some concrete details is specified using a signature which "erases" some information. You can then talk about parametricity by saying that anything that passes through that erasure process properly has to have really, truly, fully forgotten all of the information it doesn't use.

Because really that's what parametricity is. It's a property of types that says, roughly, that certain values can take a type which is maximally forgetful, or, seen from the other side, really parametric types heavily constrain the values that might be represented.

If I ask you for a type which has forgotten many details then (a) you're heavily restricted in what you can return, and (b) I can guess a lot of its properties. If I give you such a value then you can use it in many specific manners.

[dead-claudia]

@tel

So, I'd really recommend taking more points from OCaml/SML here. The thing that static-land calls a "type" is what OCaml calls a module.

Which is pretty much where I was coming from with this.

[rpominov]

@isiahmeadows @tel

Sorry, I have very little knowledge of OCaml/SML, so it's hard for me to understand what you're saying. Could you explain it in vocabulary of JavaScript and this specification? Are you suggesting that we should not add parametricity requirement, or that it should be stated somehow differently, or something else?

Edit: if this about type signatures, lets move it to #31 .

[ivenmarquardt]

@tel What do you mean with "implicit search" in terms of typeclasses? Can you provide an alternative term, so that I can google it?

[tel]

@rpominov Yeah, sorry, I should probably preface that I'm pretty far on the outside of this issue, but my name was referenced and so I happened to read the thread. I've also got a little bit of experience here in thinking through how to translate these ideas to Javascript both in some interactions I've had with the Ramda and Fantasyland folks as well as my own (experimental, abandoned) approach over at tel/js-algebraic.

So, let me start with the fast answers:

• Parametricity is extremely important in making types meaningful. It absolutely should be discussed and required.
• Parametricity is a pretty tricky topic, though, and has little to do with typeclasses. It's generally tricky because it's so broad that it can be hard to talk about and translate into formal language.
• @ivenmarqardt implicit search is the Scala term and a folk term for the idea that the compiler ought to be able to furnish values of a type automatically sometimes. It's used in Haskell to say that there's exactly one implementation of the Functor dictionary for List so any time the user asks for it (by using the ... => ... context arrow) the compiler can implicitly furnish it.

---

So first on parametricity: it's completely required to make types make much of any sense at all. Departures from parametricity can almost exactly be equated with the degree to which types are lying. The formal definition is very powerful, but the informal definition takes most weight around the semantics of type variable binding: forall a . E means that E really must hold for all possible values of a and exists a . E means E really only must hold for exactly one.

Second, the idea of values taking the type forall f . Functor f => (a -> b) -> (f a -> f b) and how it relates to parametricity seems to be a big question here. For this, I'm mentioning that implicits/typeclasses are sweeping details under the rug that make the presentation really clear. In particular, there is exactly one obvious global function of (roughly) that type which can be written very easily (in Javascript-y terms, here)

// type FunctorDict f = { map: forall a b . (a -> b) -> (f a -> f b) }

// ListFunctor : FunctorDict List
const ListFunctor = {
  map: f => l => l.map(f)
}

// forall f . FunctorDict f -> (a -> b) -> (f a -> f b)
function map(dict) { return dict.map }

This eliminates the implicit passing of the FunctorDict argument that Haskell does using typeclass machinery and makes it clear how all of these types function (also making them feel pretty useless, but bear with me). It's also essentially identical to how OCaml modules work---FunctorDict would be a module, but you can also write "dependent modules" (confusingly called "functors" in ML literature) which look like

(* fake ocaml syntax to make this a little more approachable for people with haskell familiarity *)

signature FUNCTOR = sig
  type t
  val map : forall a b . a -> b -> (t a -> t b)
end

signature EXAMPLE = sig
  type t a
  val idMap : forall a . t a -> t a
end

module Example(F : FUNCTOR): EXAMPLE = struct
  type t a = F.t a
  val idMap = F.map identity
end

Anyway, you can see how OCaml talks about "dependent modules" essentially as a function between modules. It's exactly that actually except that in order to have proper type theoretic properties we need to have the "value language" and the "module language" separate from one another.

[rpominov]

@tel This is still way over my head, but I think at least partially what you're saying is that language of this spec is far from perfect. For instance what we call "Type" should be called differently. And I'm totally agree with that!

Also I agree that because we don't have any representation of type classes in static-land, maybe Haskell isn't the best source of inspiration for developing that language and it's semantics.

Current state of the spec is as good as my current education in this areas goes, it will slowly improve as I learn more, but I'd gladly accept any help of course to boost that improvement 😄

[tel]

@rpominov I'm mostly responding to some of the questions raised above with discussing parametricity, but yeah you're right on in saying that Haskell typeclasses can pose a significant challenge to translation of these ideas into Js.

I'll bow out for the moment since I think the more focused question about parametricity is most important—but I think that this is always something of a struggle with coming to understand Haskell's representation of these kinds of laws and structures. Seeing them in other contexts like OCaml (or Agda) can be good for stripping away unessential details.

[tel]

Conversely, definitions should reflect every aspect of the values it manipulates in their types.

[rpominov]

Yea, but in our case specification provides type signatures to which implementations must fit.

[tel]

Here's a common example of a parametricity violation (and the havoc it causes)

// Assume `goodMap : (a -> b, Maybe a) -> Maybe b`

// Same type, but devious!
// badMap : (a -> b, Maybe a) -> Maybe b
function badMap(f, m) {
  if (m.value == 0) {
    return Maybe.Nothing
  } else {
    return goodMap(f, m)
  }
}

This is obviously cheating—it relies on (heterogenous) equality being defined for all values in Javascript—but nothing about the bare type variable a reflects that idea. If parametricity holds then we know certain so-called "free theorems" about the behavior of badMap, but since we've violated parametricity those will not hold.

Here's the free laws we can expect: http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi where you type in (a -> b) -> (Maybe a -> Maybe b) and click "hide type instantiations" and then look at the bottom where "Reducing all permissable relation variables to functions" has happened

-- our function is named `f`
(forall x . h (p x) = q (g x)) ==> forall x . fmap h (f p x) = f q (fmap g y) -- or
h . p = q . g ==> fmap h . f p = f q . fmap g

or, any such function should commute with fmap so long as the lifted functions commute as well. Let h = p = q = g and we'll see that any such function should commute with fmap generally.

fmap g . f g = f g . fmap g

This obvious is violated by badmap since it has special behavior which blows up on hitting a particular value and that blow-up won't commute.

[rpominov]

I don't like that it says "... to get more information about their types". When we do something like a === undefined we don't really inspect to get more information about type but rather use === operation that works with any types, so it kinda technically legitimate.

Don't know how to say it better. Any suggestions?

[dead-claudia]

@rpominov I'm not very experienced with OCaml (I've only really just toyed with it a few times), but OCaml's modules are like JavaScript's object namespaces + TypeScript's interfaces, just with a few other useful goodies (e.g. module functors = interface -> interface functions). Static Land also kind of depends on a combination of namespaces and interfaces to define its types, which is why we made the parallel. IMHO it'd probably be a bit foreign to JS developers in both OO and FP worlds, since they are generally used to TypeScript-style or Haskell-style syntax for denoting types.

(For similar reasons, the WebAssembly reference interpreter could be hard to read for those unfamiliar with OCaml syntax.)

[rpominov]

Ok, this is still not perfect but I guess it's better than nothing. I'll merge this and we can improve it later when we figure out how.