Re: Are types checked statically?

[Per Bothner <per@bothner.com>]

On 03/16/2017 10:38 AM, list+org.sourceware.kawa@io7m.com wrote:
> On 2017-03-16T10:23:24 -0700
> Per Bothner <per@bothner.com> wrote:

>> Kawa currently doesn't have "function types" - the type of all
>> functions is just 'procedure' without any specification of
>> argument or result types.  However, the following is on the wish-list:
>> https://www.gnu.org/software/kawa/Ideas-and-tasks.html#Optimized-function-types-and-values-using-MethodHandles
>
> I'm not sure I understand this fully. I'm familiar with JVM internals,
> including method handles, but the above is more an issue of efficiency
> than of correctly checking the types of functions, isn't it? Unless I'm
> mistaken, Kawa lambda expressions have the proper types and the types
> are checked statically, right? They just may not have an efficient
> underlying representation on the JVM.

It's not just performance.  A *specific* lambda expression has proper types,
and if you call a *known* procedure it is type-checked.  However, there is
no way to say "the value of this variable is an unknown function that takes
(T1 .. Tn) arguments and returns a Tr result".  That is a major part of what
the linked proposal does - in addition to enabling better code generation.
It is possible to add procedure types, and only use them for type-checking,
without optimizing the calling convention.
-- 
	--Per Bothner
per@bothner.com   http://per.bothner.com/