Conjunction disjunction, what's your function?

It's time to turn my attention to functions. Like virtually any language, Effes has functions; like any language written in the last few years, those functions are data. (At what point does the term "functional programming language" start to lose its meaning, given that every language these days incorporates FP principles?)

Every function in Effes has a type, which is just its signature. For instance, doubler(i : Int) = i * 2.0 would have a type of Int -> Double. Subtyping basically follows the Liskov substitution principle: f : Vehicle -> Door is a subtype of g : Car -> Part because you can use f anywhere you'd be able to use g.

Like data types, function types can be composed into conjunctive and disjunctive types. Take the following:

data Cat, Person
countLegs : (Cat -> Int) = c -> 4
sayHi : (Person -> String) = p -> "Hi, I'm #{p.name}"

countHi = countLegs sayHi

countHi is a conjunction of countLegs and sayHi. Invoking this function doesn't chain or compose them; only one will get invoked. Think of it as a box that contains both functions: invoking this box means opening it, taking out one of the functions, and using it.

This follows the data trait analogy: a Cat Person type refers to an object that is both a feline and a human; it also can be thought of as two separate objects stuck together. When you have a Cat Person and ask for its fur type, you're looking at its cat-like nature; when you ask for its social security number, you're looking at its person-like nature. Similarly, countHi has both a countLegs-like nature and a sayHi-like nature.

(There's a slight difference here in that a conjunctive data type can be used in functions that look at both of its aspects; this doesn't apply to functions.)

This means that the input to countHi can either be a Cat (in which case countLegs is invoked) or a Person (in which case sayHi is invoked). In the first case, the result is an Int, and in the second case it's String. Putting that together, we get a type of (Cat | Person) -> (Int | String). More generally:

(Ia -> Ra) (Ib -> Rb) : (Ia | Ib) -> (Ra | Rb)

Disjunctions follow the same analogy; a Cat | Person type refers to a single object which is a feline or person, so functional disjunctions work the same way. Imagine a type that said "I'm either countLegs or sayHi". To pass an argument into it, you'd have to guarantee that the argument could be passed to either function; it would have to be both a Cat and a Person. Depending on which function got invoked, the result would be either an Int or a String.

(Cat -> Int) | (Person -> String)
 : (Cat Person) -> (Int | String)

(I0 -> R0) | (I1 -> R1) : (I0 I1) -> (R0 | R1)

Notice the symmetry here: The input to a conjunction of functions is the disjunction of their inputs, while the input to a disjunction of functions is the conjunction of their inputs. In both cases, the result is a disjunction of their results.

One edge case is when the input to a conjunction is composed of both input types. For instance, what happens if we break out the beakers and engineer a Cat Person? If we pass it to a conjunction countLegs sayHi, both functions in that composed function can process it. Which gets to? (This isn't a problem for a disjunctive type, since its object is just a single function.)

I'm not positive how to handle this case. One solution is to have both functions process it, and then compose the result. So, passing Cat Person to countHi = countLegs sayHi would result in a (4 "Hi, I'm Yuval") : (Int String).