Are types checked statically?

Are types checked statically?

[list+org.sourceware.kawa]

[-- Attachment #1: Type: text/plain, Size: 637 bytes --]

Hello!

I'm looking for a scripting language that can be embedded into a Java
program (ideally via the JSR223 API, but this is not a hard
requirement). However, one of my requirements is static type checking
and that tends to limit the options somewhat. As someone who enjoys
functional programming, I was quite pleased to learn that Kawa existed!
However, I can't quite make out from the information on the site
whether or not the types are checked at compilation time or not. I 
appreciate that the distinction is somewhat subtle if "compilation
time" actually means "when the script is loaded by the running program".

M

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 854 bytes --]

Re: Are types checked statically?

[Per Bothner]

On 03/16/2017 10:02 AM, list+org.sourceware.kawa@io7m.com wrote:
> Hello!
>
> I'm looking for a scripting language that can be embedded into a Java
> program (ideally via the JSR223 API, but this is not a hard
> requirement). However, one of my requirements is static type checking
> and that tends to limit the options somewhat. As someone who enjoys
> functional programming, I was quite pleased to learn that Kawa existed!
> However, I can't quite make out from the information on the site
> whether or not the types are checked at compilation time or not. I
> appreciate that the distinction is somewhat subtle if "compilation
> time" actually means "when the script is loaded by the running program".

Kawa does support JSR223, though the latter is not a good match for a statically typed language.

Kawa does type-checking at compile-time, and you can either compile in
advance (to class files) or on-the-fly.
You can fine-tune this to some extent:
https://www.gnu.org/software/kawa/Options.html#Options-for-warnings-and-errors

Kawa does optimistic/lenient typing, though I'd be interested in
adding an option for strict typing:
https://www.gnu.org/software/kawa/Ideas-and-tasks.html#Optional-strict-typing-along-with-an-explicit-dynamic-type

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
-- 
	--Per Bothner
per@bothner.com   http://per.bothner.com/

Re: Are types checked statically?

[list+org.sourceware.kawa]

[-- Attachment #1: Type: text/plain, Size: 1619 bytes --]

On 2017-03-16T10:23:24 -0700
Per Bothner <per@bothner.com> wrote:
> 
> Kawa does support JSR223, though the latter is not a good match for a statically typed language.

Good to know, thanks. I've heard this sentiment expressed (of JSR223)
elsewhere too.

> Kawa does type-checking at compile-time, and you can either compile in
> advance (to class files) or on-the-fly.
> You can fine-tune this to some extent:
> https://www.gnu.org/software/kawa/Options.html#Options-for-warnings-and-errors

Very nice! This is good news.

> Kawa does optimistic/lenient typing, though I'd be interested in
> adding an option for strict typing:
> https://www.gnu.org/software/kawa/Ideas-and-tasks.html#Optional-strict-typing-along-with-an-explicit-dynamic-type

I've not used Kawa yet, so I don't know how the current typing rules
feel. Stricter checking is typically a plus in my book though.

> 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.

M

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 854 bytes --]

Re: Are types checked statically?

[Per Bothner]

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/