roy inspired statically typed, functional language for lua?

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

roy inspired statically typed, functional language for lua?

David Manura
Roy [1-3] is a functional, statically typed (Hindley–Milner/ML-style)
language that compiles to JavaScript, and it otherwise preserves
JavaScript semantics in the interest of lightweight output (in
contrast to full-scale OCaml/Haskell -> JavaScript compilers).  Given
that a number of languages compile to JavaScript (like CoffeeScript
and others [4]), some languages compile to Lua (like MoonScript [5]
and others [6]), and the similarities between Lua and JavaScript, it
would be fairly straightforward to implement a Roy-like language in
Lua.  I wonder what others think of the merits of this approach for
Lua.

A useful benchmark may be the success of Roy, but I don't see examples
of non-trivial code implemented in it yet.  As my own test, Appendix 1
shows lua-5.1.5/test/cf.lua manually translated into Roy syntax, which
Roy then automatically translates to JavaScript in Appendix 2.  Other
than the anonymous functions (which are simple to elide) and lack of
string.format (blame JavaScript), there's little overhead.  Other
examples like lua-5.1.5/test/sort.lua (list manipulation) may be
another matter.  To illustrate static type checking, omission of the
last argument to write_temp_table gives the error "Function(Number,
Number, #as) is not Function(Number, Number, Number, Number)".

The topic of static type checking and Lua has come up before [7] but
perhaps with a different emphasis of extending rather than replacing
Lua syntax.  The motivation of course is proactively reducing errors
while preserving the Lua runtime and interoperability with regular Lua
modules (much like F# on .NET).  Simple problems in Lua like static
detection of typos in local variables [8] I consider solved *and then
some* by means of the newer generation of semantic Lua text editors
(e.g. the editor syntax highlights variables by scope and usage), but
more complex analysis is still a challenge without more support from
the language.  That is why the typical suggestion for dynamic
languages has often been greater emphasis on unit testing.

[1] http://brianmckenna.org/blog/roy_ieee
[2] http://roy.brianmckenna.org/
[3] http://guide.roylang.org/
[4] http://altjs.org/
[5] http://moonscript.org/
[6] http://lua-users.org/wiki/LuaImplementations
[7] http://stackoverflow.com/questions/813926/strongly-typed-lua
[8] http://lua-users.org/wiki/DetectingUndefinedVariables

--- Appendix 1 ---

let write s =
  process.stdout.write s

let string_length s =
  (String s).length

let pad acc n =
  if (string_length acc) < n then
    pad (' ' ++ acc) n
  else
    acc

let format (x : Number) =
  let y = (Number x).toFixed 0
  pad y 3

let write_cline c cmax =
  write ( format c )
  write " "
  if c >= cmax then
    0
  else
    write_cline (c + 1) cmax

let write_fline c cmax =
  let f = (9/5)*c + 32
  write ( format f )
  write " "
  if c >= cmax then
    0
  else
    write_fline (c + 1) cmax

let write_temp_table c0 cend cstep =
  write "C "
  write_cline c0 (c0 + 9)
  write "\nF "
  write_fline c0 (c0 + 9)
  write "\n\n"
  if c0 + cstep >= cend then
    0
  else
    write_temp_table (c0 + cstep) cend cstep

let _ = write_temp_table -20 50 10

--- Appendix 2 ---

var write = function(s) {
    return process.stdout.write(s);
};
var string_length = function(s) {
    return String(s).length;
};
var pad = function(acc, n) {
    return (function() {
        if(string_length(acc) < n) {
            return pad((' ' + acc), n);
        } else {
            return acc;
        }
    })();
};
var format = function(x) {
    var y = Number(x).toFixed(0);
    return pad(y, 3);
};
var write_cline = function(c, cmax) {
    write(format(c));
    write(" ");
    return (function() {
        if(c >= cmax) {
            return 0;
        } else {
            return write_cline((c + 1), cmax);
        }
    })();
};
var write_fline = function(c, cmax) {
    var f = (9 / 5) * c + 32;
    write(format(f));
    write(" ");
    return (function() {
        if(c >= cmax) {
            return 0;
        } else {
            return write_fline((c + 1), cmax);
        }
    })();
};
var write_temp_table = function(c0, cend, cstep) {
    write("C ");
    write_cline(c0, (c0 + 9));
    write("\nF ");
    write_fline(c0, (c0 + 9));
    write("\n\n");
    return (function() {
        if(c0 + cstep >= cend) {
            return 0;
        } else {
            return write_temp_table((c0 + cstep), cend, cstep);
        }
    })();
};
var _ = write_temp_table(-20, 50, 10);
//@ sourceMappingURL=dm.js.map

Reply | Threaded
Open this post in threaded view
|

Re: roy inspired statically typed, functional language for lua?

Paul K
Hi David,

Possibly related; what is the state of the type inference logic you've
implemented in lua-inspect? From my reading of the code, you've
attempted to infer the types of values and parameters to assist with
detecting possibly invalid operations (although I haven't seen many
warnings related to that).

I'm not too excited about something like Roy for three (partially
contradictory) reasons:

1. I'm fairly happy with what I already have in Lua; I'll be even
happier camper when some of the type coercion rules go away.

2. I don't see how it helps me with errors like "local foo =
function()...end; do foo = 123 end". This is something that happened
to me at least once when I accidentally assigned something to "next"
without localizing it and it took me a good hour to figure out why my
code suddenly started failing in a completely unrelated module. In
fact, I resorted to "git bisect" to find out what really happened.

3. It doesn't go far enough for me. If we're going to implement some
form of static typing/inference, I'd prefer to see something similar
to F# that includes the notion of units
(http://blogs.msdn.com/b/andrewkennedy/archive/2008/08/29/units-of-measure-in-f-part-one-introducing-units.aspx).

In terms of the actual implementation, it may be interesting to look
at how to implement this as an optional component using static type
inference and hints (possibly in comments to preserve compatibility).

Paul.

P.S. in terms of compiling to JavaScript there is also lua.js
(https://github.com/mherkender/lua.js)

On Mon, Jul 9, 2012 at 10:21 PM, David Manura <[hidden email]> wrote:

> Roy [1-3] is a functional, statically typed (Hindley–Milner/ML-style)
> language that compiles to JavaScript, and it otherwise preserves
> JavaScript semantics in the interest of lightweight output (in
> contrast to full-scale OCaml/Haskell -> JavaScript compilers).  Given
> that a number of languages compile to JavaScript (like CoffeeScript
> and others [4]), some languages compile to Lua (like MoonScript [5]
> and others [6]), and the similarities between Lua and JavaScript, it
> would be fairly straightforward to implement a Roy-like language in
> Lua.  I wonder what others think of the merits of this approach for
> Lua.
>
> A useful benchmark may be the success of Roy, but I don't see examples
> of non-trivial code implemented in it yet.  As my own test, Appendix 1
> shows lua-5.1.5/test/cf.lua manually translated into Roy syntax, which
> Roy then automatically translates to JavaScript in Appendix 2.  Other
> than the anonymous functions (which are simple to elide) and lack of
> string.format (blame JavaScript), there's little overhead.  Other
> examples like lua-5.1.5/test/sort.lua (list manipulation) may be
> another matter.  To illustrate static type checking, omission of the
> last argument to write_temp_table gives the error "Function(Number,
> Number, #as) is not Function(Number, Number, Number, Number)".
>
> The topic of static type checking and Lua has come up before [7] but
> perhaps with a different emphasis of extending rather than replacing
> Lua syntax.  The motivation of course is proactively reducing errors
> while preserving the Lua runtime and interoperability with regular Lua
> modules (much like F# on .NET).  Simple problems in Lua like static
> detection of typos in local variables [8] I consider solved *and then
> some* by means of the newer generation of semantic Lua text editors
> (e.g. the editor syntax highlights variables by scope and usage), but
> more complex analysis is still a challenge without more support from
> the language.  That is why the typical suggestion for dynamic
> languages has often been greater emphasis on unit testing.
>
> [1] http://brianmckenna.org/blog/roy_ieee
> [2] http://roy.brianmckenna.org/
> [3] http://guide.roylang.org/
> [4] http://altjs.org/
> [5] http://moonscript.org/
> [6] http://lua-users.org/wiki/LuaImplementations
> [7] http://stackoverflow.com/questions/813926/strongly-typed-lua
> [8] http://lua-users.org/wiki/DetectingUndefinedVariables
>
> --- Appendix 1 ---
>
> let write s =
>   process.stdout.write s
>
> let string_length s =
>   (String s).length
>
> let pad acc n =
>   if (string_length acc) < n then
>     pad (' ' ++ acc) n
>   else
>     acc
>
> let format (x : Number) =
>   let y = (Number x).toFixed 0
>   pad y 3
>
> let write_cline c cmax =
>   write ( format c )
>   write " "
>   if c >= cmax then
>     0
>   else
>     write_cline (c + 1) cmax
>
> let write_fline c cmax =
>   let f = (9/5)*c + 32
>   write ( format f )
>   write " "
>   if c >= cmax then
>     0
>   else
>     write_fline (c + 1) cmax
>
> let write_temp_table c0 cend cstep =
>   write "C "
>   write_cline c0 (c0 + 9)
>   write "\nF "
>   write_fline c0 (c0 + 9)
>   write "\n\n"
>   if c0 + cstep >= cend then
>     0
>   else
>     write_temp_table (c0 + cstep) cend cstep
>
> let _ = write_temp_table -20 50 10
>
> --- Appendix 2 ---
>
> var write = function(s) {
>     return process.stdout.write(s);
> };
> var string_length = function(s) {
>     return String(s).length;
> };
> var pad = function(acc, n) {
>     return (function() {
>         if(string_length(acc) < n) {
>             return pad((' ' + acc), n);
>         } else {
>             return acc;
>         }
>     })();
> };
> var format = function(x) {
>     var y = Number(x).toFixed(0);
>     return pad(y, 3);
> };
> var write_cline = function(c, cmax) {
>     write(format(c));
>     write(" ");
>     return (function() {
>         if(c >= cmax) {
>             return 0;
>         } else {
>             return write_cline((c + 1), cmax);
>         }
>     })();
> };
> var write_fline = function(c, cmax) {
>     var f = (9 / 5) * c + 32;
>     write(format(f));
>     write(" ");
>     return (function() {
>         if(c >= cmax) {
>             return 0;
>         } else {
>             return write_fline((c + 1), cmax);
>         }
>     })();
> };
> var write_temp_table = function(c0, cend, cstep) {
>     write("C ");
>     write_cline(c0, (c0 + 9));
>     write("\nF ");
>     write_fline(c0, (c0 + 9));
>     write("\n\n");
>     return (function() {
>         if(c0 + cstep >= cend) {
>             return 0;
>         } else {
>             return write_temp_table((c0 + cstep), cend, cstep);
>         }
>     })();
> };
> var _ = write_temp_table(-20, 50, 10);
> //@ sourceMappingURL=dm.js.map
>

Reply | Threaded
Open this post in threaded view
|

Re: roy inspired statically typed, functional language for lua?

steve donovan
On Tue, Jul 10, 2012 at 8:05 AM, Paul K <[hidden email]> wrote:
> In terms of the actual implementation, it may be interesting to look
> at how to implement this as an optional component using static type
> inference and hints (possibly in comments to preserve compatibility).

There's always Roy with Lua as the compilation target ...

I agree with Paul, it would be very interesting to see a dialect of
Lua which can be statically verified. There will need to be
annotations, of course.

Some inspiration can come from the other great language from Brazil, Boo [1]:

def sqr(x as double):
    return x*x

Return type can be safely inferred, but arguments need type
annotations.  To make this generic, you need to be able to specify the
property  'behaves like a number' (either 'number' or implements the
necessary metatmethods).  Finding a sufficiently rich type notation to
capture Lua semantics would be the intellectually interesting part of
this.

steve d.

[1] an entertaining semi-Python that statically compiles to .NET/Mono assemblies

Reply | Threaded
Open this post in threaded view
|

Re: roy inspired statically typed, functional language for lua?

David Manura
In reply to this post by Paul K
On Tue, Jul 10, 2012 at 2:05 AM, Paul K <[hidden email]> wrote:
> Possibly related; what is the state of the type inference logic you've
> implemented in lua-inspect?

To give an idea, consider this contrived example:

  local function f(x)
    if x == 0 then return "a","a" else return "a","b",3 end
  end
  local function g()
    for ii=1,10 do
      local aa = math.sqrt(ii)
      local bb = aa > 0
      local cc = bb + bb
      return (f(cc))
    end
    return 5
  end
  local h = g()

`f` is seen to have two exits, and basically the unification of the
two returns implies `f` has return type ("a", `string`, `unknown`),
where `unknown` is the superset of all types.  It's deduced from the
numeric for loop that `ii` is a number.  The signature on `math.sqrt`
is therefore satisfied, and `aa` is of type number.  (If, however,
`ii` were known to be a *unique* number, then the exact value of `aa`
would be determined by actually executing the math.sqrt function,
which is marked as a pure function and therefore safe for it to
evaluate.)  A number compared to a number is a boolean, so `bb` is of
type boolean.  booleans don't support '+' (assuming no funny
debug.setmetatable on booleans), so `c` has type `error` (which you
may alert the user about).  The second return in `g` is recognized as
dead code, so return value of `g` is the result of `(f(cc))`, which is
"a".  So, `h` has value "a".  This is all done without truly executing
the `for` loop, at least in the usual way.

We also determine which variables are immutable, unused, undefined,
global/local, etc.

There are ways to inject type information with special comments
("--!"), if one so desires.  You see this in LuaInspect's own
codebase, where all AST nodes are named with a postfix "ast" in a
sort-of Hungarian notation, and this is made known to the analyzer via
a "--!" comment that indirectly calls  `context.apply_value('ast$',
ast)` to annotate all variables in lexical scope matching a name
pattern with a given mock type.

This may sound all great.  Well, no, it has the potential to be great.
A lot of stuff in the analysis may be missing, and I don't see myself
working much on this soon.  Contributors welcome.  For example, the
binary operator evaluation ("dobinop") has the knowledge that
arithmetic operations on two booleans is bad, but it currently lacks
the knowledge that indexing a number is bad.  That would be easily
added though.  Also, whether this type system is all theoretically
good by some measure, probably not, but this is a lint tool and it
needs to be useful not perfect.

> From my reading of the code, you've
> attempted to infer the types of values and parameters to assist with
> detecting possibly invalid operations (although I haven't seen many
> warnings related to that).

I don't think you currently make use of this in ZeroBrane.  (The
inferred types/values are stored in ast.value, and the HTML and SciTE
plugins display this on hover or double click via
LI.get_value_details.)

BTW, something like M.show_warnings in ZeroBrane probably would be
good to have as a standard plugin in LuaInspect.  The current plugins
(even the CSV export from the command line) generate output optimized
for consumption by editors rather than by humans using it as a batch
mode friendly lint style tool.  I think some have expected to use
LuaInspect in that latter way, but M.show_warnings is more suitable
for that.

> I'm not too excited about something like Roy for three (partially
> contradictory) reasons:
>
> 1. I'm fairly happy with what I already have in Lua; I'll be even
> happier camper when some of the type coercion rules go away.

Lacking that, type coercion could be flagged by a static analyzer in
some cases.  More simply, it would also be possible to do this
dynamically via instrumentation.  Say your test suite were to load a
custom searcher function that rewrites all `a .. b` operations with a
function call `_concat(a,b)` that is then evaluated at runtime and
prohibits conflicting types (the idea is related to
http://lua-users.org/lists/lua-l/2011-12/msg00621.html ).

> 2. I don't see how it helps me with errors like "local foo =
> function()...end; do foo = 123 end". This is something that happened
> to me at least once when I accidentally assigned something to "next"
> without localizing it and it took me a good hour to figure out why my
> code suddenly started failing in a completely unrelated module. In
> fact, I resorted to "git bisect" to find out what really happened.

But in ML style languages, variables cannot be rebound like that.

In LuaInspect, mutable and immutable variables (in terms of binding)
are flagged differently, with the mutables often highlighted in
italic.  Not that someone might really notice this unless their coding
practices made such mutables rare and highlighting settings made them
really stand out.  Ocaml's explicit "ref" (on the TODO list of Roy) is
that type of thing.  Some have said that "const" should be a default
qualifier in C++.

> 3. It doesn't go far enough for me. If we're going to implement some
> form of static typing/inference, I'd prefer to see something similar
> to F# that includes the notion of units
> (http://blogs.msdn.com/b/andrewkennedy/archive/2008/08/29/units-of-measure-in-f-part-one-introducing-units.aspx).

I've used that type of thing with a C++ analyzer.  in C/C++/D, a
related topic is "strong typedefs".  It's also related to your point
of preventing implicit type conversions between types that share the
same implementation (e.g. two types that alias to number).

> In terms of the actual implementation, it may be interesting to look
> at how to implement this as an optional component using static type
> inference and hints (possibly in comments to preserve compatibility).

Some options if, unlike Roy, one wants to stay within Lua syntax but
give hints to an analyzer:

  - special comments.  Upside: versatile and ignored by Lua `load`.
Downside: a little awkward ("--[]" looks like minus).

    local function get_distance(time --[s])
      local rate = 5 --[m/s]
      return rate * time
    end
    return get_distance(5 --[s])

  - Hungarian notation:  Upside: versatile.  Downside: could be more
implicit; m_per_s also is more verbose than m/s

    local function get_distance(time_s)
      local rate_m_per_s = 5
      return rate_m_per_s * time_s
    end
    local time_s = 5
    return get_distance(time_s)

    - unit constants: Upside: natural syntax.  Downside: how to
specify function parameter types?

    local S = 1
    local M = 1 -- dummy variables, intended only for analysis

    local function get_distance(time)
      local rate = 5*M/S
      return rate * time
    end
    return get_distance(5 * S)