One pattern that I have frequently used in EMACS elisp is that redefining a top-level value overwrites that value rather than shadowing it. Basically hot reloading. This doesn't work in a dependently typed context as the type of subsequent definitions can depend on values of earlier definitions.
def t := string
def x: t := "asdf"
redef t := int
redefining t here would cause x to fail to type check. So the only options are to either shadow the variable t, or have redefinitions type-check all terms whose types depend on the value being redefined.Excluding the type-level debugging they mention, I think a lean style language-server is a better approach. Otherwise you are basically using an append-only ed to edit your environment rather than a vi.
- Static typing a la Haskell with Coalton in Common Lisp
- Dependent typing with Deputy in Clojure (this post)
- The Common Lisp compiler SBCL ported to the Nintendo Switch
- Common Lisp and AI/deep learning
- A special retrospective on Modula and Oberon
- Many lightning talks.
Peter Norvig, 1992
Paradigms of AI Programming: Case Studies in Common Lisp
https://en.m.wikipedia.org/wiki/Peter_Norvig
it's no coincidence Google is actively maintaining sbcl, either.
droideqa•4h ago
The only hint is this repo[0] referenced in the paper.
[0]: https://gitlab.com/fredokun/deputy
agumonkey•2h ago