~technomancy/fennel

8 5

Typed Fennel

Rudolf Adamkovič <salutis@me.com>
Details
Message ID
<m2ttwwxsg3.fsf@me.com>
DKIM signature
missing
Download raw message
Greetings, fellow hackers!

As we use more Fennel at Egghead Games, we feel the need for static
typing.  In addition to letting us write fewer tests, it would also
allow us to generate type-safe native wrappers for mobile, avoiding
unnecessary crashes in production.  We could contribute work to the
Fennel compiler, if this is something that would be accepted.

So, we would like to open a discussion on the topic.

(1) The built-in types

  The eight basic types of Lua
    nil, boolean, number, string, function, userdata, thread, table

  The bottom type
    any

  The 'or' operator for combining types, as in
    (or number string nil)

  The 'type?' alias for the common type
    (or type nil)

(2) New types

  (type seller number)           ;; a simple type
  (type result number?)          ;; a simple optional type
  (type grades {number string})  ;; a table
  (type scores [number])         ;; a sequential table

  Supporting literals in the type position, if possible, would unlock a
  lot of real-world benefits, such as

  (type person {:age number :name string}) ;; a record
  (type results {: result true})           ;; a set

  Like the {} and [] syntax specializes the 'table' basic type, we need
  something to specialize the 'function' type.  Perhaps 'fn', as in

    (type predicate (fn [any...] boolean))

(3) Attaching types to symbols

  Similar to 'declaim' in Common Lisp.

  ;; declare the type of a function
  (check math.type [any] string?)

  ;; declare the type of a variable
  (check math.pi number)

  ;; declare the type of variadic arguments
  (check table.pack [any...] table)

  ;; declare the type of a multi-valued return
  (check table.unpack [table number? number?] (values any))

  Some other names for 'check' that come to mind:

         (is math.pi number)
    (declare math.pi number)
      (prove math.pi number)
      (proof math.pi number)

(4) The compiler

  The compiler would perform automatic type checking upon compilation
  and also provide a compile-time API for getting type information.

  Further, the compiler would declare the types for all symbols in the
  ten standard libraries that ship with Lua.  The libraries are tiny, so
  this would be a few pages of 'check' forms, maybe per Lua version.

Let us discuss!

Rudy
-- 
"'Contrariwise,' continued Tweedledee, 'if it was so, it might be; and
if it were so, it would be; but as it isn't, it ain't.  That's logic.'"
-- Lewis Carroll, Through the Looking Glass, 1871/1872

Rudolf Adamkovič <salutis@me.com> [he/him]
Studenohorská 25
84103 Bratislava
Slovakia
Details
Message ID
<875y9b4m4n.fsf@hagelb.org>
In-Reply-To
<m2ttwwxsg3.fsf@me.com> (view parent)
DKIM signature
missing
Download raw message
Rudolf Adamkovič <salutis@me.com> writes:

> As we use more Fennel at Egghead Games, we feel the need for static
> typing.  In addition to letting us write fewer tests, it would also
> allow us to generate type-safe native wrappers for mobile, avoiding
> unnecessary crashes in production.  We could contribute work to the
> Fennel compiler, if this is something that would be accepted.

This is something I've thought about for a while.

I don't think it's a good idea to add this to the Fennel compiler any
time soon. I won't rule it out in the very long term, but it would need
to spend a lot of time evolving on its own before getting added to
Fennel itself due to the backwards-compatibility guarantees we make.

We have a plugin system that would be a great fit for this. The static
analysis performed by the fennel-ls language server uses the plugin
system to great effect. It's likely that a type system would need more 
extension points than the language server, so that would certainly
require changes to the compiler to accomplish, but as long as we can
agree on where those go, it's easy.

There's a linter in the Fennel repository which also serves as a
demonstration of the plugin system:

    https://git.sr.ht/~technomancy/fennel/tree/main/src/linter.fnl

The biggest problem here is that I've never seen a type system design
which actually fits the problems that Fennel/Lua face. The main successful
gradual type systems out there are Typed Racket and Erlang's Dialyzer,
but both those languages are *very* different from Lua in that they
strongly prefer record types which have fields specified at compile time
over free-form maps, and they do not have any concept of nil in the
language. Taking a design which works for Racket and adapting it to a
different language that makes heavy use of nil is fraught with peril, as
I believe we've seen with Typed Clojure. Many things that are easy or at
least viable in Racket are only viable because of the lack of nil.

One option is to go the route of Teal and just ignore nil altogether by
treating every type as implicitly unioned with nil. I don't believe this
is a good idea; nils are by far the most common source of type errors,
so a type system which just doesn't even try to prevent the most common
sort of errors is of very limited use. It doesn't seem worth bothering.

I don't have nearly enough understanding of type theory to design a
system that's good enough to live up to my standards. Maybe that just
means my standards are unrealistically high. However...

I think what I'd recommend at this point is some thorough deep dives
into the prior art. Don't try to reimplement Teal without first
understanding its shortcomings and why they chose to make those
decisions. If it's truly an inherent difficulty in the Lua type system
that prevents nil-checking from being viable, don't bother reinventing
the wheel; just create a bridge from Fennel to Teal. If you think you
can identify where Teal went wrong, maybe you can do better, but that
should be your starting point rather than a from-scratch design.

The traditional approach with type systems is to try to prove the
correctness of the system; this is very difficult in situations with a
lot of uncertainty, which gradual typing makes worse, and unioning nil
with every type makes MUCH worse. One promising alternative is to
instead attempt to prove contradictions in the types. (success typing)
This is the method used by Dialyzer, and I believe it's likely that the
issues with nil that plague the more conventional approach might be more
manageable with this approach.

Dialyzer's approach also allows inference to cross function boundaries,
whereas the approach of Teal and Typed Racket requires a lot of
annotation to be useful. This means you can use Dialyzer to effectively
find bugs even on an Erlang codebase that's completely dynamic where the
authors have never even heard of Dialyzer. But of course annotations
can help it find *more* bugs.

    https://learnyousomeerlang.com/dialyzer

Honestly if I had a year-long sabbatical with a chance to focus on a
Big Problem, I would probably spend it researching success typing and
trying my hand at implementing it in Fennel.

>   Supporting literals in the type position, if possible, would unlock a
>   lot of real-world benefits, such as
>
>   (type person {:age number :name string}) ;; a record
>   (type results {: result true})           ;; a set

I think this is smart! It leads to a more unified-looking declaration
than the way Teal handles records.

> (3) Attaching types to symbols
>
>   Similar to 'declaim' in Common Lisp.
>
>   ;; declare the type of a function
>   (check math.type [any] string?)

The docstring functionality in Fennel is built using a general-purpose
metadata system which allows functions but also other arbitrary values
to have metadata maps associated with them. This could be a natural
place to store types, but it is normally a runtime feature rather than a
compile-time feature. However, it's possible to access the metadata of
functions specifically at compile time, but no such mechanism exists for
tables. I'm not convinced this is the right place to store type
information, but it's definitely worth considering. The APIs to store
and retrieve this information already exist today.

>   Further, the compiler would declare the types for all symbols in the
>   ten standard libraries that ship with Lua.  The libraries are tiny, so
>   this would be a few pages of 'check' forms, maybe per Lua version.

Depending on the compatibility of the underlying representation, it
might be possible to get a lot of this data from Teal. They have
annotations for not only Lua's standard library, but also a good number
of 3rd-party libraries and IIRC frameworks like love2d as well.

-Phil
Details
Message ID
<5BE94BA1-56E7-44E1-B7B3-017E0C04E60D@pobox.com>
In-Reply-To
<875y9b4m4n.fsf@hagelb.org> (view parent)
DKIM signature
missing
Download raw message
It is many years since I had even a cursory knowledge of type systems 
and their
theory and application, so I won’t pretend to offer solution 
suggestions.
However, I can chime in with a view of requirements that hopefully is 
relevant.

In our specific need (using Fennel to implement a shared core used by 
Swift in
iOS apps and Kotlin or Java in Android apps), we have multiple source 
files that
end with an Interface declaration, e.g.:

   ;;; Theme Interface

   {: title
    : launch-effects
    : count-items
    : item
    : set!
    : get}

Currently, we call these using syntax like:

   luaNil("theme", "set!", value);

There's no type checking in this scenario, so we could, say, pass a 
numeric
value when a string is expected.  We would like to instead be able to 
create
host language specific wrappers to instead have a call like this, say:

   LuaThemeSet(value)

where luaThemeSet has a return type of whatever is closest to Nil (e.g. 
void)
and only takes a string (in this case).

My simple brain says, since implementing a fennel type system is "non 
trivial",
could it make sense to have some annotation system in this interface 
section
that would meet our immediate need to create wrappers, but, it could 
also be
used to add more functionality in the future.  E.g. a linter could 
attempt code
analysis to confirm/deny the accuracy of the annotation.  Or, simpler, 
it could
evaluate Fennel callers of the module to see if they're using it in a 
way that
matches the annotation (confirming parameter counts would be a good 
start
perhaps?).

I write this without looking at Teal.  Perhaps there is a Teal 
annotation that
could be applied to the interface declaration that could pass-through to 
the
generated Lua code, and *that* could be used to generate wrappers, and 
also
participate in whatever analysis benefits that Teal provides across the 
Lua
code.

TLDR, I wonder if there's some incremental thing we can do now that 
provides
some immediate benefits, but also moves towards and informs a more 
complete
solution?

Cheers, Michael
Details
Message ID
<A262C71A-9F15-4F11-B456-A2B566BA091B@pobox.com>
In-Reply-To
<875y9b4m4n.fsf@hagelb.org> (view parent)
DKIM signature
missing
Download raw message
(Re-sent with a more compatible line length. Sorry!)

It is many years since I had even a cursory knowledge of type systems
and their theory and application, so I won’t pretend to offer solution
suggestions.  However, I can chime in with a view of requirements that
hopefully is relevant.

In our specific need (using Fennel to implement a shared core used by
Swift in iOS apps and Kotlin or Java in Android apps), we have multiple
source files that end with an Interface declaration, e.g.:

  ;;; Interface

  {: title
   : launch-effects
   : count-items
   : item
   : set!
   : get}

Currently, we call these using syntax like:

  luaNil("theme", "set!", value);

There's no type checking in this scenario, so we could, say, pass a
numeric value when a string is expected.  We would like to instead be
able to create host language specific wrappers to instead have a call
like this, say:

  LuaThemeSet(value)

where luaThemeSet has a return type of whatever is closest to Nil (e.g.
void) and only takes a string (in this case).

My simple brain says, since implementing a fennel type system is "non
trivial", could it make sense to have some annotation system in this
interface section that would meet our immediate need to create wrappers,
but, it could also be used to add more functionality in the future.
E.g. a linter could attempt code analysis to confirm/deny the accuracy
of the annotation.  Or, simpler, it could evaluate Fennel callers of the
module to see if they're using it in a way that matches the annotation
(confirming parameter counts would be a good start perhaps?).

I write this without looking at Teal.  Perhaps there is a Teal
annotation that could be applied to the interface declaration that could
pass-through to the generated Lua code, and *that* could be used to
generate wrappers, and also participate in whatever analysis benefits
that Teal provides across the Lua code.

TLDR, I wonder if there's some incremental thing we can do now that
provides some immediate benefits, but also moves towards and informs a
more complete solution?
Details
Message ID
<6B8E3D0D-1000-4394-AE2B-DB97A746A5FB@gmail.com>
In-Reply-To
<A262C71A-9F15-4F11-B456-A2B566BA091B@pobox.com> (view parent)
DKIM signature
missing
Download raw message
>My simple brain says, since implementing a fennel type system is "non
>trivial", could it make sense to have some annotation system in this
>interface section that would meet our immediate need to create wrappers,
>but, it could also be used to add more functionality in the future.

Fennel has a concept of metadata, that can be attached to functions, e.g. the 
docstring, or arglist, and it is possible to add arbitrary metadata via the table 
syntax:

(fn f [x]
  {:typed/args [:int] :typed/ret :string}
  (tostring x))

This metadata can be analyzed via some external tool that simply loads the 
code and checks all functions. Which leads to:

>E.g. a linter could attempt code analysis to confirm/deny the accuracy
>of the annotation. 

>TLDR, I wonder if there's some incremental thing we can do now that
>provides some immediate benefits, but also moves towards and informs a
>more complete solution?

So yeah, I think metadata is that incremental thing.


-- 
Andrey Listopadov
Details
Message ID
<8BD54124-0E6C-431A-B0FF-B283ED57E0C3@pobox.com>
In-Reply-To
<875y9b4m4n.fsf@hagelb.org> (view parent)
DKIM signature
missing
Download raw message
> yeah, I think metadata is that incremental thing.

Thanks!  If I understand this correctly, metadata can be arbitrary, and
only fnl/arglist is already defined (along with fnl/docstring).  To
build a collection of tools, it would be helpful to agree on some extra
terms.  Or perhaps the example you provided is already in use? I.e.
typed/args and typed/ret (though I’m guessing it was for illustration)?

At least then, the next step becomes clear: propose some terms, start
using them and then iterate as we learn from real world usage.
Details
Message ID
<3B8AF734-58C4-4316-A839-9EFDBC7D0191@gmail.com>
In-Reply-To
<8BD54124-0E6C-431A-B0FF-B283ED57E0C3@pobox.com> (view parent)
DKIM signature
missing
Download raw message
>Thanks!  If I understand this correctly, metadata can be arbitrary, and
>only fnl/arglist is already defined (along with fnl/docstring).  

Correct. There were some thoughts on using {:fnl/deprecated "ver"} or just
:deprecated too, but I don't think it's already in the core.

>To build a collection of tools, it would be helpful to agree on some extra
>terms.  Or perhaps the example you provided is already in use? I.e.
>typed/args and typed/ret (though I’m guessing it was for illustration)?

This was purely to illustrate the way it can potentially be used.  I think a tool
should emerge first, and with sufficient popularity the metadata will stick.
Something akin to CIDER's indentation specification[1], which is supported 
outside CIDER too.  This way the evolution of tooling is natural and interest-based.

[1]: https://docs.cider.mx/cider/indent_spec.html

-- 
Andrey Listopadov
Rudolf Adamkovič <salutis@me.com>
Details
Message ID
<m2a5ylvxq6.fsf@me.com>
In-Reply-To
<A262C71A-9F15-4F11-B456-A2B566BA091B@pobox.com> (view parent)
DKIM signature
missing
Download raw message
Michael Mee <mikemee@pobox.com> writes:

> TLDR, I wonder if there's some incremental thing we can do now that
> provides some immediate benefits, but also moves towards and informs a
> more complete solution?

Perhaps an incremental solution could be a bunch of macros that
type-check at run time, using assertions.  We could extract the type
signatures for the wrappers and also get some implicit safety.

Rudy
-- 
"Logic is a science of the necessary laws of thought, without which no
employment of the understanding and the reason takes place."
-- Immanuel Kant, 1785

Rudolf Adamkovič <salutis@me.com> [he/him]
Studenohorská 25
84103 Bratislava
Slovakia
Details
Message ID
<CAEXOEF05w_xdgvc3V31cmX=7cE+kjjr-aGEukpxvtDL-3wqwNg@mail.gmail.com>
In-Reply-To
<m2a5ylvxq6.fsf@me.com> (view parent)
DKIM signature
missing
Download raw message
Random thought: Would there be any merit in implementing a system
similar to Clojure's spec library, or similar
3rd party libraries for Fennel?

Off the top of my head...

- Specs have value in any context: Validation at runtime, static
analysis during development,
  generating data for testing

- Seems like it would play nice with lua being effectively a table of
functions assigned to keys

- Tooling doesn't need to touch the compiler itself, people can build
an ecosystem around
   those specs

Having learned Clojure before learning TypeScript for work, I have not
been enjoying it. While it does nicely reduce
the possibility of introducing the common `cannot read 'name' of
undefined` type of errors, the team I'm on has been
spending the past month or so solving bugs that have valid types, but
make incorrect assumptions about the world
around them, or have made it more difficult to implement the correct
behavior because of the type complexity. This
has started to make me appreciate spec more because it does have
meaning and value at compile time, development
time, and even runtime as needed to enforce and test those assumptions.

Anyway, I just thought I'd throw that idea out there.

On Wed, May 3, 2023 at 6:47 PM Rudolf Adamkovič <salutis@me.com> wrote:
>
> Michael Mee <mikemee@pobox.com> writes:
>
> > TLDR, I wonder if there's some incremental thing we can do now that
> > provides some immediate benefits, but also moves towards and informs a
> > more complete solution?
>
> Perhaps an incremental solution could be a bunch of macros that
> type-check at run time, using assertions.  We could extract the type
> signatures for the wrappers and also get some implicit safety.
>
> Rudy
> --
> "Logic is a science of the necessary laws of thought, without which no
> employment of the understanding and the reason takes place."
> -- Immanuel Kant, 1785
>
> Rudolf Adamkovič <salutis@me.com> [he/him]
> Studenohorská 25
> 84103 Bratislava
> Slovakia
Reply to thread Export thread (mbox)