BLisp: A Statically Typed Lisp Like Language(ytakano.github.io) |
BLisp: A Statically Typed Lisp Like Language(ytakano.github.io) |
Also, is there an example of the type inference working?
For example you may want to query a database with a custom filter predicate function. If you pass one of BLisp's `Pure` functions across the wire, the database could execute the function with relative safety (compared with using `eval` with a string, or whatever).
I find it frustrating that almost all popular languages lack any safe facility for this, so people have to create some limited query schema (with it's own custom wire encoding and mini-interpretter), or instantiate a sandbox for a non-pure language like Lua and eval a string, or else invent their own fully-blown programming language along the lines of BLisp.
I don't equate S-expressions with macros. S-expressions make many things easier, including: simple and regular but expressive syntax, expressive function and variable names with basically any character sequence allowed, copy and paste-able code that just works, easy automatic code formatting.
For statically typed languages, they only feel ergonomic to me if they have highly specialized syntax and if they really leverage the type-system (which is often in conflict with macros and runtime flexibility).
I completely agree with the idea that their power is derived from macros, but I vehemently disagree that macros are incompatible with a static type system. The type of a form can be just a simple ADT
data Form = FInt Int
| FCons Form Form
| FNil
| FString String
| ...
(defmacro double (x)
`(* x x))
(defmacro double (x)
(FCons '* (FCons x (FCons x FNil))))
double :: Form -> Form
> `(* x x))
Two bugs in two lines. Lisp is indeed a powerful language.
Why would it not just be a normal function then?
EDIT: here's an example of a discussion about that in Rust: https://github.com/rust-lang/unsafe-code-guidelines/issues/2...
I'm now designing macros, but I cannot spend sufficient time to do. Anyway, macros will be implemented in the near future.
This language is being implemented for bare-metal or no_std environments in Rust. This is often called shell. I don't want to control OSes or devices by YAML or unsafe scripting languages.
In any case, it looks neat, I think the intersection of static types and Lisps is a space that needs more experimentation with, so I'm happy to see that.
I hope eventually it gains more effects as well, with only Pure and IO, you can't do much of the cool things that effect systems bring.
so I would guess interpreted
What that means is: I might call a function that tells me it will give me type X but instead it blows up. It's good that it blows up btw - that is the best thing a language with gradual typing can do for these cases. But it's not something I would be satisfied with.
Now, you can say that "blowing up" is part of any function anyways, but then my response would be that this severely hurts my ability to reason about how code will behave when run, so I'm giving up a huge benefit of a static type-system in general.
* most crucially, x isn't actually spliced in, meaning that the macro always literally expands to (+ x x). For example, (+ (double 2) 5) just expands to (+ (+ x x) 5), which will either crash if x is undefined or do something unexpected if x is.
* Even if x were spliced in properly, it gets evaluated twice. That's wasteful at best, and if x has some kind of side effect you (arguably) would get unexpected behaviour - the side effects would run twice.
(defmacro double (x)
(let ((temp (gensym))
`(let ((,temp ,x))
(+ temp temp))))
(let ((#:uniqueName123 (parse-integer (read-line)))
(+ #:uniqueName123 #:unique_symbol_123))
To explain a little bit what is going on: normally if you want to have an s-expression as a piece of data, you can use the quote special form - (quote (a b c)), usually shortened to '(a b c), returns a list containing three symbols (think of these as special strings), "a", "b", "c". If you want instead to evaluate a variable named "a", you can use the ` syntax, together with , and ,@. That is, `(,a b ,@c) will produce a list containing the value of a variable named "a", the symbol "b", and the value of a variable named "c", spliced in. If a is '(1 2 3) and c is '(4 5 6), `(,a b ,@c) will return the 5-element list ((1 2 3) b 4 5 6). Depending on how this is used further, b itself may be evaluated or just printed as is.
So, when expanding the macro, x will be initialized to the form provided as argument to double (not the value of that form). Then, temp will first be assigned a value that is produced by gensym, which generates a unique symbol; then, we'll return a list that represents some Lisp code binding the form represented by x to a variable whose name is the value returned by gensym, and then using this same variable name in a call to +. Finally, if this macro was "called" from regular lisp code, the expression it returned will be compiled or interpreted.
The macro could also be called from a special form like macroexpand-1, which would just return the list returned by the macro, without evaluating it; or macroexpand, which would do the same but recursively until there are no more macros in the expansion.
Note: a symbol is basically a string that can be used as a Lisp identifier, and is registered as such in the Lisp runtime. It is a separate type from string, but you can create a string from a symbol, or try to create a symbol from a string (which fails if the string is not a valid Lisp identifier).
Make that three bugs. The macro is called "double," but the numeric result is square.
I think to clarify what I said - I didn't mean that static typing and macros are excluding each other. But I think you can either have a sound static type system and highly restricted macros, or less restricted macros but only an unsound type system. That's what I meant with "conflict".
I'm interested to hear though why you think unrestricted macros make the type system unsound. Can you explain? The code generated by macros would be type-checked in the scheme I described, and type-unsafe code can't be executed by the macro itself, so it seems safe to me.
But in LISP they are called and expanded implicitly, with the compiler/interpretter keeping track of what's what.
(let ((#:uniqueName123 (parse-integer (read-line)))
(+ #:uniqueName123 #:uniqueName123)) (defmacro double (x)
(let ((temp (gensym))
`(let ((,temp ,x))
(+ ,temp ,temp)))) (compile nil '(lambda (x) (double x)))
;Compiler warnings :
; In an anonymous lambda form: Undeclared free variable TEMP
; In an anonymous lambda form: Unused lexical variable #:G520
Note, this is a warning and not an error because of CL's semantics, as the following is a valid program:
(let ((temp 100))
(double 10))
;returns 200
(declaim (special temp))
(compile 'nil (lambda (x) (double x))
;Compiler warnings :
; In an anonymous lambda form: Unused lexical variable #:G524Now, that doesn't have to mean that there is some inherential that stops the combination from super powerful macros and sound statical types from working together, but if anything, there is at least a compromise to be made in terms of resources, because it seems you would have to put a lot of effort into it.
> The code generated by macros would be type-checked in the scheme I described, and type-unsafe code can't be executed by the macro itself
Well, I would already consider this to be quite a big restriction though.
For my part, my sense is that it would be appropriate for a static lisp to choose completeness over soundness in its type system. Gödel's incompleteness theorem tells us that a static type checker can't be both sound and complete. So you've got to pick one, and there's something about sacrificing liberty for the sake of security that strikes me as being fundamentally un-lispy. All the talk further up about CL-style unhygienic macros seems like a good illustration of the relevant culture. You can't ignore Scheme and Racket, of course, but the longer tradition in Lisp is to say, "We'll give you all the power and all the footguns, and leave it up to you to use them responsibly."
Which part, the type-checking? Don't we want it to be type-checked?