Enforce parametricity - Githubissues

rpominov commented 7 years ago

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

davidchambers commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

@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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

@rpominov

@isiahmeadows Yeah, you're probably right here.

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

rpominov commented 7 years ago

@isiahmeadows This was a response to https://github.com/rpominov/static-land/pull/30#issuecomment-255522229

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

davidchambers commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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

I'm sorry for making an unhelpful comment.

ivenmarquardt commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

@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 commented 7 years ago

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 commented 7 years ago

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

tel commented 7 years ago

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 commented 7 years ago

@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 commented 7 years ago

@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 commented 7 years ago

@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 commented 7 years ago

@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 commented 7 years ago

@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 commented 7 years ago

@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.

dead-claudia commented 7 years ago

@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 commented 7 years ago

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.

fantasyland / static-land

Enforce parametricity #30

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

On to my point