Co/contravariance for function schemas?

[nilern]

From working on coercion subtyping I would assume that a function schema encoder would be something like

(fn [f] (fn [x] (output-encoder (f (input-decoder x)))))

and decoder

(fn [f] (fn [x] (output-decoder (f (input-encoder x)))))

but currently they are no-ops.

Of course type-theoretic intuitions might not translate to a dynamic language. I think function schemas are a bit weird anyway since they can only be checked by calling the function.

[frenchy64]

This seems right. For example, encoding a string->int function to be int->string (psuedocode):

(encode [:=> [:cat string?] int?]
        str->int
        (function-transformer
          (cat-transformer (int-transformer))
          (string-transformer)))
=> (fn [& args]
     (encode int?
             (apply
               str->int
               (decode [:cat string?]
                       (cat-transformer (int-transformer))
                       args))
             (string-transformer)))

And decoding it back to string->int.

(decode [:=> [:cat string?] int?]
        int->str
        (function-transformer
          (cat-transformer (int-transformer))
          (string-transformer)))
=> (fn [& args]
     (decode int?
             (apply
               int->str
               (encode [:cat string?]
                       (cat-transformer (int-transformer))
                       args))
             (int-transformer)))

This might open a can of worms wrt. performance (eg., wrapping wrappers). There are some nice papers to mitigate some of the cost, see space-efficient contracts and coercions. An example written in Clojure.

Of course type-theoretic intuitions might not translate to a dynamic language. I think function schemas are a bit weird anyway since they can only be checked by calling the function.

Yes, perhaps. I think something weird (unsound) needs to be done for m/validate where no wrapping is allowed, but here we're allowed to use the standard contra/covariant rules used in higher-order contracts via wrapping. It seems sensible enough (not to comment on whether it should be included in malli :) ).

One interesting (new) part to me is the relationship between the schemas and the transformers. I tried to write some typing rules. As you say, this seems related to coercions, which I only have a passing familiarity with.

                    X->Y :- [:=> X Y]
(:decoder A-transformer) :- [:=> A X]
(:encoder B-transformer) :- [:=> Y B]
=====================================
(encode [:=> X Y]
        X->Y
        (function-transformer
          A-transformer
          B-transformer))
:- [:=> A B]

                    A->B :- [:=> A B]
(:encoder A-transformer) :- [:=> X A]
(:decoder B-transformer) :- [:=> B Y]
=====================================
(decode [:=> X Y]
        A->B
        (function-transformer
          A-transformer
          B-transformer))
:- [:=> X Y]

(For those new to typing rules, read e :- t as "expression e has schema t" and

condition1
condition2
==========
consequent

as "if condition1 and condition2, then consequent".)