Smoothing type functions and value functions

Maybe it is a bit late (8 month from last post!), but I re-read this post yesterday, and something came to my mind.

One of the roots of this post is depicting the similarity between value functions and type functions. While a value function defines the relation between input and output value types, a type function defines the relation between input and output type types. Smooth as silk!

But the way we express value functions and type functions don’t match that much. Let’s review the signature for defining functions in Ceylon:
– Named value function

Float addFloats(Float x, Float y) => x+y;

– Named type function:

alias Pair<Value> given Value satisfies Object => [Value,Value]; 

– Anonymous value function

(Float x, Float y) => x+y

– Anonymous type function

 <Value> given Value satisfies Object => [Value,Value] 

Looking for regularity

If the original post presents the homogeneity between type and value functions, I would like to propose homogeneity between those can be represented.

I can see two sources of irregularity:

Providing output types:

As far as I can see, “providing output type” can be understood as “providing a description for the output”.

Named value functions are the only ones that allow providing the output type (despite you can delegate it to the compiler). So I can’t really see a reason why I cant write anonymous value functions like “Float(Float x, Float y) => x+y”.

Even more, describing the output is not just providing a type, but providing the description (or the restrictions) the output must satisfy. So one should be able to ‘downcast’ the result to something like “Number(Float x, Float y) => x+y”, the same way we do when writing function headers.

For type functions, providing output type isn’t that straightforward. What is the type of the ‘type value’ on the right of the fat arrow? Digging a bit into Ceylon class hierarchy, we can see that Tuples satisfy Sequence, so in our example, we can use Sequence<Object>.

Clever reader may ask: “Why Sequence<Object>? Why not Sequence<Value>?” Running an analogy with value functions show the reason: Would you write “Sequence<x> gimmeASequenceWith(Float x)”? No! ‘x’ is a value, not a type! But you will use the restriction on the input to obtain the restriction on the output, like “Sequence<Float> gimmeASequenceWith(Float x)”.

Given that, we can rewrite the previous function definitions:
– Named value function: Allow optionally ‘downcasting’

Number addFloats(Float x, Float y) => x+y;

– Named type function: We can get rid of ‘alias’ keyword

Sequence<Object> Pair<Value> given Value satisfies Object => [Value,Value];

– Anonymous value function: Allow providing output type and optionally ‘downcasting’

Number(Float x, Float y) => x+y

– Anonymous type function: Allow providing output type

Sequence<Object><Value> given Value satisfies Object => [Value,Value] 

Note to self: This last definition clearly looks like a curried function! It can be understood as a type function that, given a type <Value> , returns another type function that, given a type <Object>, returns a Sequence type!

Locality for input restrictions:

One thing really disturbs me when writing code is locality. Definition should be close to defined, usage should be close to definition, etc… Without locality, you should go up and down the code, looking for the meta.

In value functions, definition for the parameters is just beside the parameter itself. In the value function example, definition for parameter ‘x’ is just besides it, in the form of the ‘Float’ type. Well done!

But in type functions, this is not the case. The restrictions on the input types should be provided ‘later’ with a given clause! This also means to verbosely repeating the name of the input type! What would you thing about the following value function definition?

    Number addFloats(x,y) given x satisfies Float & y satisfies Float => x+y;

The meaning is the same, but the definition look too verbose.So, what if we apply the concept of locality to type parameters in type functions?

    Sequence<Object> Pair<Object Value> => [Value,Value];

At first sight, it may seem confusing two types inside the “<>”. But when you realize that “Value” is not a type but a type value, things start to make a bit more sense. Maybe using a ‘variable-like’ name makes things clearer:

    Sequence<Object> Pair<Object X> => [X,X];

So getting back to the sample signatures, we can rewrite them again:
– Named value function:

Number addFloats(Float x, Float y) => x+y;

– Named type function:

Sequence<Object> Pair<Object Value> => [Value,Value];

– Anonymous value function:

Number(Float x, Float y) => x+y

– Anonymous type function:

Sequence<Object><Object Value> => [Value,Value] 

Summarizing:

So, if we accept all the proposed changes (output types for all and locality for input types), functions can be parsed by the following pseudo-grammar:
For value functions:

 [OutputType|'function'] FunctionName? '(' [InputType InputName]* ')' => ...

And for type functions:

 [OutputType|'alias'] FunctionName? '<' [InputType InputName]* '>' => ...

Really regular, isn’t it?

2 thoughts on “Smoothing type functions and value functions

  1. So my reaction to this is:

    1. Providing a “return type” for a type function is misleading and wrong. The “returned” type for Pair isn’t Sequence it is [Value, Value]. Indeed, just like with another important type of function (a class), or even like a function with an inferred return type, we don’t need to explicitly write in a return type, so we use a keyword instead. (In this case “alias” instead of “class” or “function”.)

    2. Writing the constraints on a type parameter in the type parameter list instead of in the separate “satisfies” clause is, a priori, perfectly reasonable. However, it really gets messy once you start to consider, recursive upper-bound relationships, enumerated bounds, type-function type parameters, etc. And so as a purely practical matter I strongly prefer to declare type parameters in a separate “given” clause.

    Like

  2. 1. The question behind all of this is: why value functions allow explicit return type? Shouldn’t we always return the canonical type (inferred) satisfying the definition?

    Abstract functions( ‘formal’ in Ceylon) are the answer. They provide a way for defining the header of a function, but delegating the body to ‘refining’ functions.
    It is easy to see that type inference does not work for abstract functions. So returning type should be explicit on them.
    If we want to provide regularity between value functions and type functions, we should be able to define abstract type functions, and hence returning type should be explicit.

    Abstract value functions also allow to declare a ‘supertype’ as the return type. I.E. returning Collection instead of List. In other words, abstract value functions are saying “it can return any value that satisfies this (super)type”. Abstract type functions should be able to do the same, but replacing “…any value that satisfies…” by “…any type that satisfies…”.
    In fact, even actual value functions can declare a ‘supertype’ as the return type, when they are intended to be refined. Why shouldn’t type functions work the same way?

    Summarizing, type inference works great, but only when a) there is a body for inferring type from and b) the type inferred from this body is the canonical type for all functions ‘refining’ the current one.

    2. All those situations do complicate the reading for constraints, despite putting them in the parameter list or in a separate clause. I do agree that moving them to a non-inline clause improves readability in complex case, but make it more verbose for simpler (most common) cases.
    Given that proposal is just syntax sugar for the most generic “satisfies” case, maybe it is worth considering using it for the simpler cases, or even let the writer choose the one according situation.
    Not a big change nor a big deal.

    Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s