Syntax for reification of types

Hi all,

I've got a little language with a syntax resembling C#. It is statically typed, and performs type inference. Functions are polymorphic, and don't require the type of the arguments to be explicit. I am trying to avoid dynamic typing as much as possible. Functions are reified during function invocation based on the inferred type of the arguments. In order to pass a function as an argument, or store it in a variable, I need a convenient way of performing the reificiation.

Here is the syntax that I am considering:


var fxn1 = (int, int) -> (x, y) => x * y;
var fxn2 = (int, int) -> Multiply;
var fxn3 = (int[3][], float[3][]) -> ComputeNormals;

As in C# the "=>" operator represent the lambda operator but here the symbol "->" now represents the function reification operator. Does this make sense? Any other suggestions or examples of how it is done in other languages?

Thanks in advance!

Comment viewing options

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

Being stored in a variable,

Being stored in a variable, why doesn't Multiply know the type of its arguments? And similarly, why do you not type the arguments as you're defining the lambda?

var fxn1 = (int x, int y) => x*y;

Good questions

Hi Matt,

Multiply could be an integer multiply, a floating point multiply, etc., and so forth. I don't want users to have to worry about that. I want users to be able to write code without worrying about the type of arguments.

It might make sense for me to allow unreified functions to be assigned to variables, and to have the user perform reification at a later point. This is why I like the idea of a reification as an operator.

In the current language prototype lambdas are only usable in a limited set of contexts (e.g. filter, map, fold, and zip operations).

"Has-type" operator

In Haskell and friends we can use "x :: y" to declare that "x" has type "y". The nicest thing about this 'operator' is that we can use it on sub-expressions and allow the rest to be inferred. For example:

-- Arguments are Ints
\(x :: Int) (y :: Int) -> someFunction x y

-- Arguments can be used as Ints
\x y -> someFunction (x :: Int) (y :: Int)

-- someFunction turns Ints into a Float
\x y -> (someFunction :: Int -> Int -> Float) x y

-- Our whole function turns Ints into a Float
(\x y -> someFunction x y) :: Int -> Int -> Float

Thanks for sharing

Thanks for sharing. It nicely illuminates a feature of Haskell that I didn't previously understand very well.

Does your language have an

Does your language have an explicit notion of function types (eg. "Int -> Int", "Float -> String -> Double", "(Int -> Int) -> ((Float -> Bool) -> String) -> List (Bool -> Bool)")? You say that functions' types can be inferred from the types of their arguments; with function types you can also go the other way ("x must be an Int, since it's being passed to a function of type 'Int -> Bool'").

Does your language have some way to express typing constraints/relationships? This allows polymorphism without losing the precision required for safety and inference (ie. without having to become dynamic). Some examples are the placeholder variables used by ML and its derivatives, eg. a function of type "a -> Int -> a" accepts one argument of any type and another argument of type Int, and its return value must be of the same type as the first argument.

I've also played with typing constraints based on illative combinatory logic, which essentially uses a fe primitive functions (combinators) to build other functions at the same time as their types eg. see http://www.encyclopediaofmath.org/index.php/Illative_combinatory_logic . This would be quite a radical departure from a C#-style language, but it's always good to know more than one way of doing something, to avoid cargo-cult programming :)

> Does your language have

> Does your language have some way to express typing constraints/relationships?

No, not at the current time. I wonder if it is going to be inevitable in the end.

While I'm building the prototype I'm currently baking high-level operators (map, zip, filter, reduce, etc.) into the language semantics and type-inference engine. Right now they are the only consumers of functions as values.

This is clearly inelegant and not scalable but it is helping me get a working language created more quickly and keeping the core simple.

> This allows polymorphism without losing the precision required for safety and inference (ie. without having to become dynamic)

I haven't convinced myself that one has to provide explicit constraints in order to avoid unsafe construct in a programming language. Right now, I'm completely avoiding any dynamic typing. The result is a very limited language (no recursive functions, no recursive types, etc.) but which is still quite useful in some limited domains (e.g. array processing).