Are types checked statically?

classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Are types checked statically?

Mark Raynsford
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

attachment0 (871 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Are types checked statically?

Per Bothner
On 03/16/2017 10:02 AM, [hidden email] 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
[hidden email]   http://per.bothner.com/
Reply | Threaded
Open this post in threaded view
|

Re: Are types checked statically?

Mark Raynsford
On 2017-03-16T10:23:24 -0700
Per Bothner <[hidden email]> 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

attachment0 (871 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Are types checked statically?

Per Bothner
On 03/16/2017 10:38 AM, [hidden email] wrote:
> On 2017-03-16T10:23:24 -0700
> Per Bothner <[hidden email]> 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
[hidden email]   http://per.bothner.com/