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

3 hours 13 min ago

8 hours 3 min ago

15 hours 27 min ago

1 day 2 hours ago

1 day 8 hours ago

1 day 8 hours ago

1 day 9 hours ago

1 day 9 hours ago

1 day 10 hours ago

1 day 10 hours ago