[pansa2]

> function returns should be contravariant

I'm not very familiar with these relations, but shouldn't function returns be covariant? `String => Cat` is a subtype of `String => Animal`?

> Function parameters should be covariant

For function parameters, doesn't it depend on how the parameter is used?

[paldepind2]

> I'm not very familiar with these relations, but shouldn't function returns be covariant? `String => Cat` is a subtype of `String => Animal`?

You're right :) I mixed up covariance and contravariance for function parameters and return value in my comment.

> For function parameters, doesn't it depend on how the parameter is used?

I don't think so, but maybe there's specific circumstances I don't know of? Function parameter types is a constraint on _input_ to the function. Changing that to a subtype amounts to the function receiving arguments that satisfies a stronger constraint. That seems that something that would hold no matter how the parameter is used?

[pansa2]

> > For function parameters, doesn't it depend on how the parameter is used?

> I don't think so, but maybe there's specific circumstances I don't know of?

I don't know specific circumstances either, but I presume they exist because of things like Dart's `covariant` keyword [0], which makes function parameters covariant instead of contravariant.

[0] https://dart.dev/language/type-system#covariant-keyword

[sparkie]

The use case would be where the arguments are expected to be filled in by the function - ie, as additional return types.

Consider if we have `A <= B <= C`, and a function:

    int Copy([out] Array<B> dest, [in] Array<B> src);

Given some potential inputs:

    Buffer<A> asrc = ...
    Buffer<B> bsrc = ...
    Buffer<C> csrc = ...

    Buffer<A> adest = allocate(...)
    Buffer<B> bdest = allocate(...)
    Buffer<C> cdest = allocate(...)

The following should be true:

    Copy(adest, asrc); // No! - How would Copy know how to copy `A` values when it only knows about `B`?
    Copy(adest, bsrc); // No! - src argument is OK, but how can it downcast them to `A`?
    Copy(adest, csrc); // No! - Same as above, and src elements must be at least `B`s`.
    
    Copy(bdest, asrc); // Ok. - Any `A` in the src are interpreted as `B`s.
    Copy(bdest, bsrc); // Ok, - all values are interpreted as `B`s.
    Copy(bdest, csrc); // No! - Argument elements must be at least `B`s`.
    
    Copy(cdest, asrc); // Ok - values are interpreted as `B`s in src, and as `C`s in dest.
    Copy(cdest, bsrc); // Ok
    Copy(cdest, csrc); // No! Argument elements must be at least `B`s`.

If the `dest` argument were contravariant, it would permit invalid copies and forbid valid ones.

    Copy(adest, asrc); // pass (wrong)
    Copy(adest, bsrc); // pass (wrong)
    Copy(adest, csrc); // fail
    
    Copy(bdest, asrc); // pass
    Copy(bdest, bsrc); // pass
    Copy(bdest, csrc); // fail
    
    Copy(cdest, asrc); // fail (wrong)
    Copy(cdest, bsrc); // fail (wrong)
    Copy(cdest, csrc); // fail

In a purely functional setting, you should not need a covariant parameter type because all writes would end up in the return type.

    copy : Array<B> -> Array<B>

[kragen]

Maybe this is intentionally introducing logical unsoundness into Dart's type system for pragmatic purposes, perhaps supplemented with some implicit dynamic checks?

[hmry]

Read-only parameters should be contravariant, write-only parameters should be covariant, and read-write parameters should be invariant.

[sparkie]

`String => Cat` and `String => Animal` are the types of the functions themselves - not the arg and return types.

If we consider inside the function:

    foo : arg:String => result:Animal
    foo = 
        ;; arg <: String
        ;; Animal <: result

However, outside of the function, when calling it, the opposite is true.

    let result = foo (arg)
        ;; String <: arg
        ;; result <: Animal

It's easy to get them mixed up when looking at it from the wrong perspective - but we should be looking at functions from the outside, not the inside - so yes, parameters should be contravariant and return types covariant.

[pansa2]

> parameters should be contravariant

Always? In that case, do you know why Dart has a `covariant` keyword [0], which makes function parameters covariant?

[0] https://dart.dev/language/type-system#covariant-keyword