Home » forums » LtU Forum

Unifying map and mapM through subtyping?

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?)

By Douglas McClean at 2010-02-26 02:58 | LtU Forum | previous forum topic | next forum topic | other blogs | 3847 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Type family tricks

You can do some fun tricks with type families. Then you can create true identity and composition functors.

The problem is that you have to help the type checker, because it can't tell which functor you mean when you say a -> a, it could be Identity, or the composition of Identity and Identity etc.

Perhaps playing with this code might give some insights in what problems you might encounter when constructing a language like you propose.

{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-}

import Prelude hiding (Functor(..), Monad(..))

-- Functor definition
type family F f a :: *
class Functor f where
  fmap :: f -> (a -> b) -> F f a -> F f b

-- Identity functor
data Id = Id
type instance F Id a = a
instance Functor Id where
  fmap Id f = f
  
-- Functor composition
data f :.: g = f :.: g
type instance F (f :.: g) a = F f (F g a)
instance (Functor f, Functor g) => Functor (f :.: g) where
  fmap (f :.: g) = fmap f . fmap g

test1 = fmap (Id :.: Id) (+1) 2

class Functor m => Monad m where
  return :: m -> a -> F m a
  bind :: m -> F m a -> (a -> F m b) -> F m b
  
instance Monad Id where
  return Id a = a
  bind Id a f = f a

test2 = 
  bind Id 1 $ \x ->
  bind Id 2 $ \y ->
  return Id (x + y)

By Sjoerd Visscher at Sat, 2010-02-27 18:33 | login or register to post comments

Great idea

That's a great idea, Sjoerd, thanks a lot!

By Douglas McClean at Sat, 2010-02-27 23:18 | login or register to post comments

Arity-polymorphism

If you have arity-polymorphism (as well described in Arity-Generic Datatype-Generic Programming) at the level of type constructors (which is not described in the above paper!), then these unifications are less troublesome. Hopefully someone will do that particular combination soon - I could use it.

By Jacques Carette at Sun, 2010-02-28 14:57 | login or register to post comments