emacs-elsa / Elsa

Emacs Lisp Static Analyzer and gradual type system.
GNU General Public License v3.0
640 stars 26 forks source link

Issue executing Elsa via. Cask #179

Open ethan-leba opened 2 years ago

ethan-leba commented 2 years ago

I saw this repo is getting some new commits (which is awesome!) so wanted to test out the new syntax, however I was unable to get it working properly. I may be missing something basic, but here's my steps to repro:

  1. Clone the repo
  2. cask install
  3. Make a file with the following contents:
    (defun add-one (x)
    (declare (elsa (int) int))
    (1+ x))
  4. Run cask exec elsa <file>
  5. Expect no errors, receive:
    scratch.el:3:23:error:reference to free variable `int'.
    scratch.el:4:3:error:argument 1 accepts type (or number marker) but received mixed
Fuco1 commented 2 years ago

Yea, the declare syntax is the part which doesn't work :D (I commented in another issue). I'm in the process of updating the documentation.

The problem is that I don't know how to get the declare forms work without having Elsa installed and loaded. Which is one of my hard requirements, to be able to analyze/annotate code which does not assume Elsa exists (like 3rd party packages where we can't convince the maintainer to adopt and support it).

tldr syntax is:

;; (add-one :: (function (int) int))
(defun add-one (x)
  (1+ x))

This is not 100% final and if we come up with nicer syntax it might be changed in the future. You can browse the code and see the annotations used in Elsa itself.

Fuco1 commented 2 years ago

But the weird part is that you didn't get an error about the unknown declare form. Maybe that only happens when the code is compiled... hmm... I'll have to check it out.

ethan-leba commented 2 years ago

Ah okay, that explains that then! Works fine with the comment syntax now :)

The problem is that I don't know how to get the declare forms work without having Elsa installed and loaded. Which is one of my hard requirements, to be able to analyze/annotate code which does not assume Elsa exists (like 3rd party packages where we can't convince the maintainer to adopt and support it).

Is this about the defun/macro-declarations-alist business? I had a thought on avoiding that issue:

(declare (elsa (int) int))
(defun add-one (x)
  (1+ x))

This would also work for defvars which could be nice.

Fuco1 commented 2 years ago

The reason why I wanted to use declare is that it is inside the function, so that during refactoring it would be fairly impossible to forget to move it together (like when moving a function to another file). Comment can be forgotten, as happened to me while using php and javascript with comment annotations.

Yesterday I got an idea that maybe we could push it into the docstring, either as a one liner or as some extended syntax. The first version would provide useful if we wanted to auto-generate api reference, as it is very easily machine processable.

;; maybe could use less java-inspired syntax :D
(defun add-one (x)
  "Add 1 to number

@param int x
@return int"
  (1+ x))

;; or just use the current syntax as a one liner
(defun add-one (x)
  "Add 1 to number

elsa: (function (int) int)"
  (1+ x))
ethan-leba commented 2 years ago

Including the annotations in the docstrings is interesting, could provide some value to folks who are using dependencies that use elsa but aren't using it themselves.

If elsa ends up going with types that are inside of comments/strings, it might be best to reduce parentheses as much as possible -- lispy turns off it's features inside of strings/comments which makes working with sexps not very fun (i assume this is true for paredit/smartparens as well?)

One approach I think is worth reconsidering is annotation macros:

(defmacro elsa-deftype (name type) nil)
(defmacro elsa-type (type) nil)
(defmacro elsa-cast (type expr) expr)
(eval-when-compile (require 'elsa-annotations))

(elsa-deftype numstr (or int str))

(defun add-one (foo)
  (elsa-type (function (numstr) int))
  (1+ (elsa-cast int foo))))

This wouldn't require elsa as a dependency for those using byte-compiled packages but would be required as a dev dependency. In exchange it would afford much more flexibility to Elsa -- for example, attempting to cast a value would likely be very cumbersome just using comments (re: #180). Maybe an acceptable tradeoff?

Fuco1 commented 2 years ago

Yea, this is something that crossed my mind but I didn't spend much time on how to implementit. I didn't consider compile type macros, that might work fine.

Smartparens works with sexps inside comments by default but it can be configured not to. However, I agree that the parens can become a problem, especially when nesting composite types, such as functions, unions and constants all together, it's very clumsy.

The original haskell-inspired notation solved this nicely but wasn't a great fit for the community. So we'll have to come up with something lisp-like but not overwhelming at the same time.