In a Haskell-like language, could we unify `map :: (a -> b) -> [a] -> [b]`

and `mapM :: (Monad m) => (a -> b) -> [a] -> m [b]`

(and all the similar pairs like filter/filterM, fold/foldM, ...) by adopting the monadic definitions with the "normal" (suffix-free) names and extending the type system to allow implicit conversion into and out of the Identity monad?

It seems that such conversions aren't as problematic as a general subtyping system, since proving confluence isn't a problem. We'd have to do something to prevent the typechecker from looping indefinitely trying to unify `a`

with `Identity a`

by way of `Identity (Identity (Identity (Identity (... a ...))))`

, but I'm not sure that this would be a problem in practice. (Perhaps by avoiding an explicit transitivity-of-subtyping deduction rule, keeping the Identity-introduction, Identity-elimination, and reflexivity rules as the only deduction rules, and proving that transitivity follows from this?)

Are there other difficulties that this approach might cause? What sort of trickery might be needed to convince an optimizer over a *typed* intermediate language that the Identity introduction and elimination functions should have no operational effect? (Furthermore, is it true that they should have no effect, or is there a useful distinction between `_|_ :: Identity a`

and `Identity _|_ :: Identity a`

?)

## Recent comments

1 hour 35 min ago

2 hours 59 min ago

4 hours 27 min ago

5 hours 37 min ago

6 hours 17 min ago

9 hours 6 min ago

10 hours 10 min ago

12 hours 30 min ago

18 hours 2 min ago

19 hours 15 min ago