@@ -11,7 +11,8 @@ use crate::evidence::Evidence;
1111use crate :: source:: derive:: builder:: DerivedTreeBuilder ;
1212use crate :: source:: derive:: field;
1313use crate :: source:: derive:: variance:: {
14- ConstructorRecipe , RecordFieldRecipe , TraversalOperation , TraversalParameter , VarianceRecipe ,
14+ ConstructorRecipe , RecordFieldRecipe , TraversalOperation , TraversalParameter , Variance ,
15+ VarianceRecipe ,
1516} ;
1617use crate :: source:: terms:: ElaboratedExpression ;
1718use crate :: state:: CheckState ;
@@ -325,10 +326,10 @@ where
325326 } ;
326327 Ok ( Some ( self . builder . subtype ( mapped, target_type) ?) )
327328 }
328- TraversalOperation :: UnaryApplication { argument , .. } => {
329- // Map delegates traversal of a unary type constructor to its existing
330- // Functor instance. The generator only needs to produce the transformation
331- // that its map implementation applies to each contained value .
329+ TraversalOperation :: UnaryApplication { argument_variance , argument } => {
330+ // A covariant edge delegates to `map`; a contravariant edge reverses the
331+ // source-to-target obligation and delegates to `cmap`. The examples below
332+ // trace the covariant case .
332333 //
333334 // NonEmpty
334335 //
@@ -386,21 +387,28 @@ where
386387 // transformer :: { item :: a } -> { item :: b }
387388 // transformer = \element ->
388389 // element { item = function element.item }
389- let argument_context = TraversalContext {
390- source_type : source_argument,
391- target_type : target_argument,
392- function_depth,
390+ let argument_context = match argument_variance {
391+ Variance :: Covariant => TraversalContext {
392+ source_type : source_argument,
393+ target_type : target_argument,
394+ function_depth,
395+ } ,
396+ Variance :: Contravariant => TraversalContext {
397+ source_type : target_argument,
398+ target_type : source_argument,
399+ function_depth,
400+ } ,
393401 } ;
394402 let Some ( transformer) = self . emit_transformer ( argument, argument_context) ? else {
395403 return Ok ( None ) ;
396404 } ;
397405
398- // Resolve the polymorphic, constrained map declaration and specialize it
399- // through application. Applying `transformer` solves the element types;
400- // applying `source` solves the fresh constructor variable, specializing
401- // its wanted Functor evidence.
406+ // Resolve the operation selected by the edge variance. Applying
407+ // `transformer` solves the element types; applying `source` solves the
408+ // fresh constructor variable and specializes the wanted evidence.
402409 //
403410 // map :: forall f a b. Functor f => (a -> b) -> f a -> f b
411+ // cmap :: forall f a b. Contravariant f => (b -> a) -> f a -> f b
404412 //
405413 // NonEmpty
406414 //
@@ -426,25 +434,29 @@ where
426434 // map function (Inventory items) =
427435 // Inventory
428436 // (map (\element -> element { item = function element.item }) items)
429- let Some ( map) = self . builder . context . known_terms . map else {
437+ let operation = match argument_variance {
438+ Variance :: Covariant => self . builder . context . known_terms . map ,
439+ Variance :: Contravariant => self . builder . context . known_terms . cmap ,
440+ } ;
441+ let Some ( operation) = operation else {
430442 return Ok ( None ) ;
431443 } ;
432- let map = self . builder . term_reference ( map ) ?;
433- let Some ( map ) = self . builder . apply ( map , transformer) ? else {
444+ let operation = self . builder . term_reference ( operation ) ?;
445+ let Some ( operation ) = self . builder . apply ( operation , transformer) ? else {
434446 return Ok ( None ) ;
435447 } ;
436- let Some ( mapped) = self . builder . apply ( map , value) ? else {
448+ let Some ( mapped) = self . builder . apply ( operation , value) ? else {
437449 return Ok ( None ) ;
438450 } ;
439451
440452 // Check the specialized result against the target established above.
441453 Ok ( Some ( self . builder . subtype ( mapped, target_type) ?) )
442454 }
443- TraversalOperation :: BinaryApplication { arguments , .. } => {
444- // Bimap lifts transformations through the first and second arguments of a
445- // binary type constructor. See `emit_bimap ` for the staged construction.
455+ TraversalOperation :: BinaryApplication { first_variance , arguments } => {
456+ // Bimap and dimap lift transformations through a binary type constructor.
457+ // See `emit_binary_application ` for the staged construction.
446458 let ( first, second) = arguments. operations ( ) ;
447- self . emit_bimap ( first, second, value, traversal)
459+ self . emit_binary_application ( * first_variance , first, second, value, traversal)
448460 }
449461 // Function types require both covariant and contravariant transformations.
450462 // Given:
@@ -620,11 +632,10 @@ where
620632 operation : & TraversalOperation ,
621633 traversal : TraversalContext ,
622634 ) -> QueryResult < Option < ElaboratedExpression > > {
623- // Map and bimap require a function that transforms the inside of their source type
624- // into the inside of their target type. Bind one source value, emit its traversal,
625- // and return the resulting lambda to the map or bimap call site. A Parameter
626- // operation eta-expands its mapping expression; nested operations produce a more
627- // involved body.
635+ // Each unary or binary traversal operation requires a transformer between its
636+ // argument types. The caller has already oriented source and target according to
637+ // the edge variance. A Parameter operation eta-expands its mapping expression;
638+ // nested operations produce a more involved body.
628639 //
629640 // source :: a
630641 // target :: b
@@ -646,13 +657,18 @@ where
646657 Ok ( Some ( self . builder . lambda ( function, vec ! [ input] , body) ) )
647658 }
648659
649- fn emit_bimap (
660+ fn emit_binary_application (
650661 & mut self ,
662+ first_variance : Variance ,
651663 first : Option < & TraversalOperation > ,
652664 second : Option < & TraversalOperation > ,
653665 value : ElaboratedExpression ,
654666 traversal : TraversalContext ,
655667 ) -> QueryResult < Option < ElaboratedExpression > > {
668+ // A covariant binary edge delegates to `bimap`. A Profunctor edge reverses the
669+ // first argument obligation and delegates to `dimap`; its second argument remains
670+ // covariant. The examples below trace the Bifunctor case.
671+
656672 // Decompose both arguments of the binary type application.
657673 //
658674 // firstFunction :: a -> c
@@ -728,10 +744,17 @@ where
728744 //
729745 // firstTransformer :: Array a -> Array c
730746 // firstTransformer = map firstFunction
731- let first_context = TraversalContext {
732- source_type : source_first,
733- target_type : target_first,
734- function_depth : traversal. function_depth ,
747+ let first_context = match first_variance {
748+ Variance :: Covariant => TraversalContext {
749+ source_type : source_first,
750+ target_type : target_first,
751+ function_depth : traversal. function_depth ,
752+ } ,
753+ Variance :: Contravariant => TraversalContext {
754+ source_type : target_first,
755+ target_type : source_first,
756+ function_depth : traversal. function_depth ,
757+ } ,
735758 } ;
736759 let first_transformer = if let Some ( first) = first {
737760 let Some ( transformer) = self . emit_transformer ( first, first_context) ? else {
@@ -778,9 +801,8 @@ where
778801 None => self . emit_identity ( second_context) ?,
779802 } ;
780803
781- // Resolve the polymorphic, constrained bimap declaration and specialize it through
782- // application. Applying the source solves the fresh constructor variable and
783- // specializes its wanted Bifunctor evidence.
804+ // Resolve the operation selected by the first argument's variance. Applying the
805+ // source solves the fresh constructor variable and specializes its wanted evidence.
784806 //
785807 // bimap :: forall f a b c d.
786808 // Bifunctor f => (a -> b) -> (c -> d) -> f a c -> f b d
@@ -805,24 +827,28 @@ where
805827 // (map firstFunction)
806828 // (\record -> record { item = secondFunction record.item })
807829 // pair)
808- let Some ( bimap) = self . builder . context . known_terms . bimap else {
830+ let operation = match first_variance {
831+ Variance :: Covariant => self . builder . context . known_terms . bimap ,
832+ Variance :: Contravariant => self . builder . context . known_terms . dimap ,
833+ } ;
834+ let Some ( operation) = operation else {
809835 return Ok ( None ) ;
810836 } ;
811- let bimap = self . builder . term_reference ( bimap ) ?;
812- let Some ( bimap ) = self . builder . apply ( bimap , first_transformer) ? else {
837+ let operation = self . builder . term_reference ( operation ) ?;
838+ let Some ( operation ) = self . builder . apply ( operation , first_transformer) ? else {
813839 return Ok ( None ) ;
814840 } ;
815- let Some ( bimap ) = self . builder . apply ( bimap , second_transformer) ? else {
841+ let Some ( operation ) = self . builder . apply ( operation , second_transformer) ? else {
816842 return Ok ( None ) ;
817843 } ;
818- let Some ( mapped) = self . builder . apply ( bimap , value) ? else { return Ok ( None ) } ;
844+ let Some ( mapped) = self . builder . apply ( operation , value) ? else { return Ok ( None ) } ;
819845 Ok ( Some ( self . builder . subtype ( mapped, traversal. target_type ) ?) )
820846 }
821847
822848 fn emit_identity ( & mut self , traversal : TraversalContext ) -> QueryResult < ElaboratedExpression > {
823- // Bimap still requires a transformer for an argument that omits the traversed
824- // parameter, so supply identity rather than treating the missing operation as a
825- // missing expression.
849+ // Binary operations still require a transformer for an argument that omits the
850+ // traversed parameter, so supply identity rather than treating the missing operation
851+ // as a missing expression.
826852 //
827853 // LeftPair
828854 //
0 commit comments