Lambda types

[EasyArray]

• Lambda functions assume type "e" if not given a type
• Therefore numerical functions like [λ n . n+1] will throw an error when given numbers.
• We actually don't have a type (a SemType) for numbers
• Adding one more complication, we do have a SemType (t) for 0 and 1.

[havijw]

With some very brief testing, I was able to apply lambdas to numbers. In particular, the following worked:

[λ x . x + 1](2)
f = [λ x . x + 1]
f(2)

The output was 3 for both.

[EasyArray]

Yes, but I had to explicitly disable the type-checking this year. See https://github.com/EasyArray/phosphorus/blob/52b7050063eb9f85f82ec0528d200188e23b1548/phosphorus/phival.py#L236-L237 which I commented out in commit 87ee79fc6da8fff47e4cacd39887eae1f8849b3d .

[havijw]

I was just thinking about this while looking through the LambdaVal.__call__ function. Maybe a way to handle this is to make a SemType for numbers (which could, and probably should, just be e), and when passing to lambda's, if something of type t gets passed to a function that should take numbers, we could just change the input to have the number type and use that for the rest. So 0 and 1 would be possible values of the number type, but 0 and 1 would be interpreted as type t by default.

[EasyArray]

I keep waffling between using "n" for numbers or "e". Either way, though, your suggestion is a bit like automatic casting of a item compatible with two types. I wonder if we can generalize between just this "0" and "1" issue if we think about it that way?

[EasyArray]

It would be odd to simply type in 1 and get the type t out, since 1 is most commonly thought of as a number. Even weirder to define a function like [λn . n+1] but when you call it on 0 you get something of type t instead of n (or # or whatever).

Maybe the very easiest solution would be to allow untyped lambda functions or define a wildcard/general type like *. So [λn/* . foo] would accept any input. That way we could still infer type e when no type at all is given.

Alternatively, we could infer the lambda function is untyped / type * in most cases, but infer e if the variable is named x, y, or z?