I've been working with Church encoding recently and when I look at a typical type
newtype ChurchMaybe a =
ChurchMaybe { runChurchMaybe :: forall r . r -> (a -> r) -> r }
it looks as if functions with an existential type (runChurchMaybe) might behave similarly to functions that are polymorphic in their return type. I haven't fully understood the logic behind existential types though. So I am probably wrong.
Now I've often read that monads are less useful in untyped languages like Javascript, also because of the lack of return type polymorphism. So I wondered if I can ease this shortcoming:
// JS version of Haskell's read
// read :: String -> forall r . (String -> r) -> r
const read = x => cons => cons(x);
// option type
const Some = x => r => f => f(x);
const None = r => f => r;
console.log(
read(prompt("any string")) (Array.of) // [a]
);
console.log(
read(prompt("any string")) (Some) // Some(a)
);
console.log(
read(prompt("number string")) (x => Number(x)) // Number
);
const append_ = x => y => append => append(x) (y);
const all = x => y => x && y;
const any = x => y => x || y;
const add = x => y => x + y;
const semigroup = append_(true) (false)
semigroup(all); // false
semigroup(any); // true
semigroup(add); // 1Obviously, read isn't polymorphic in its return type, because it always returns a lambda. However, this lambda can serve as a proxy of the actual return value and the context is now able to determine what type this proxy actually produces by passing a suitable constructor.
And while read can produce any type, append_ is limited to types that have a semigroup constraint.
Of course there is now a little noise in the context of such functions, since they return a proxy instead of the actual result.
Is this essentially the mechanism behind the term "return type polymorphism"? This subject seems to be quite complex and so I guess I am missing something. Any help is appreciated.
In a comment I made an assertion without justifying myself: I said that return type polymorphism isn't a meaningful concept in an untyped language. That was rude of me and I apologise for being so brusque. What I meant was something rather more subtle than what I said, so please allow me to attempt to make amends for my poor communication by explaining in more detail what I was trying to get at. (I hope this answer doesn't come across as condescending; I don't know your base level of knowledge so I'm going to start at the beginning.)
When Haskellers say "return type polymorphism", they're referring to one particular effect of the type class dispatch mechanism. It comes about as the interplay between dictionary passing and bidirectional type inference. (I'm going to ignore polymorphic _|_s like undefined :: forall a. a or let x = x in x :: forall a. a. They don't really count.)
First, note that type class instances in Haskell are syntactic sugar for explicit dictionary passing. By the time GHC translates your program into its Core intermediate representation, all the type classes are gone. They are replaced with "dictionary" records and passed around as regular explicit arguments; => is represented at runtime as ->. So code like
class Eq a where
(==) :: a -> a -> Bool
instance Eq Bool where
True == True = True
False == False = True
_ == _ = False
headEq :: Eq a => a -> [a] -> Bool
headEq _ [] = False
headEq x (y:_) = x == y
main = print $ headEq True [False]
is translated into something like
-- The class declaration is translated into a regular record type. (D for Dictionary)
data EqD a = EqD { eq :: a -> a -> Bool }
-- The instance is translated into a top-level value of that type
eqDBool :: EqD Bool
eqDBool = EqD { eq = eq }
where eq True True = True
eq False False = True
eq _ _ = False
-- the Eq constraint is translated into a regular dictionary argument
headEq :: EqD a -> a -> [a] -> Bool
headEq _ _ [] = False
headEq eqD x (y:_) = eq eqD x y
-- the elaborator sees you're calling headEq with a ~ Bool and passes in Bool's instance dictionary
main = print $ headEq eqDBool True [False]
It works because of instance coherence: every constraint has at most one "best" matching instance (unless you switch on IncoherentInstances, which is usually a bad idea). At the call site of an overloaded function, the elaborator looks at the constraint's type parameter, searches for an instance matching that constraint - either a top-level instance or a constraint that's in scope - and passes in the single corresponding dictionary as an argument. (For more on the notion of instance coherence I recommend this talk by Ed Kmett. It's quite advanced - it took me a couple of watches to grasp his point - but it's full of insight.)
Much of the time, as in headEq, the constraint's type parameters can be determined by looking only at the types of the overloaded function's arguments, but in the case of polymorphic return values (such as read :: Read a => String -> a or mempty :: Monoid m => m) the typing information has to come from the call site's context. This works via the usual mechanism of bidirectional type inference: GHC looks at the return value's usages, generates and solves unification constraints to figure out its type, and then uses that type to search for an instance. It makes for a kinda magical developer experience: you write mempty and the machine figures out from the context which mempty you meant!
(Incidentally, that's why show . read :: String -> String is forbidden. show and read are type class methods, whose concrete implementation isn't known without any clues about the type at which they're being used. The intermediate type in show . read - the one you're reading into and then showing from - is ambiguous, so GHC doesn't know how to choose an instance dictionary in order to generate runtime code.)
So "return type polymorphism" is actually a slightly misleading term. It's really a by-word for a particular kind of type-directed code generation; its Core representation is just as a regular function whose return type can be determined from the type of its (dictionary) argument. In a language without type classes (or a language without types at all, like JS), you have to simulate type classes with explicit dictionary parameters that are manually passed around by the programmer, as @4Castle has demonstrated in another answer. You can't do type-directed code generation without types to be directed by!