The Racket platform has Typed Racket, by Sam Tobin-Hochstadt, et al.
Typed Lisp, A Primer (2019)
11–20 of 31 posts
Re: Typed Lisp, A Primer (2019)
#12Earlier quoted context omitted.
Can you explain what you mean by ‘holes for areas like that’? I assume the area you are referring to is lists as code, but I don’t understand what you are saying by claiming there needs to be a hole for it.
By a hole I mean places where it doesn't require strict typing. For example in most static languages everything is typed to some degree. Some cases they abuse things like "just make it an object" but to me that has always felt an unfortunate hole that I wish wasn't necessary but I dunno how you get around some form of it in cases like param arrays or this code as data issue.
I get it, sorry, I kind of defaulted to a more specific concept of hole in a type theoretic context.
Code as data is, while not simple in a type theoretic context, pretty well researched. I think the most promising method for achieving semantics relatively close to Lisp's `code type` is the modal type theory work from the early 2000's. It starts (according to most accounts) with Pfenning and Davies work from '94-'95 [1], then moves over to Taha,Sheard,et al's work circa 2000 on MetaML[2]. Then I think the work by Kim, et al in 2006[3] which led to Murase's work in 2017[4].
This line of work delves pretty deeply into the proof-theoretic foundations and type-theoretic of macros as a well founded element of programming languages. However, I am a firm believer in the theory of best fit for this sort of problem. A large amount of the work is based on a relatively small amount of primitive concepts, and in a language like Lisp with imperative features and mutable state, a safe implementation that is algorithmically checkable should be possible, without attempting to prove the categorical semantics of the construct.
Long story short, I think that a 'safe' and useable typed syntactic macro construct should not be thought of as intractable, but approached with sensible guide rails to implementation and then used as needed by developers.
[1] - https://dl.acm.org/doi/pdf/10.1145/237721.237788 (A Modal Analysis of Staged Computation [Davies,Pfenning 2001] [2] - https://www.sciencedirect.com/science/article/pii/S030439750... (MetaML and multi-stage programming with explicit annotations [Taha,Sheard 2000] [3] - http://kwangkeunyi.snu.ac.kr/paper/06-popl-kiyicr.pdf (A Polymorphic Modal Type System for Lisp-Like Multi-Staged Languages [Kim,etal 2006]) [4] - https://lfmtp.org/workshops/2017/inc/slides/murase.pdf (slides from a talk)
Re: Typed Lisp, A Primer (2019)
#13Yes. With macros and runtime logic it's possible to implement just about any type system in Lisp, even an ML-like system. Box everything and use macros to transparently pick it apart and reconstruct your wrapped type objects when you use them. My initial reaction to that whole idea was horror. The inefficiency! But maybe not necessarily. A compiler that understood the type system used, could optimize most of it away. Just like how Haskell or SML compilers do.
Re: Typed Lisp, A Primer (2019)
#14I've been thinking about typed lisp a bit lately since I started messing with CL again, and I admit the point about lists as code hadn't crossed my mind as something you have to deal with for any typing attempts. If you tried to make a "fully static typed lisp" likely you'd need a few holes for areas like that where they don't make sense. Well that or do the shenanigans things like c# do for param arrays where it is…
holes in the Idris sense, as in this spec?
Re: Typed Lisp, A Primer (2019)
#15Yes. With macros and runtime logic it's possible to implement just about any type system in Lisp, even an ML-like system. Box everything and use macros to transparently pick it apart and reconstruct your wrapped type objects when you use them. My initial reaction to that whole idea was horror. The inefficiency! But maybe not necessarily. A compiler that understood the type system used, could optimize most of it away.…
It exists. Qi, Coalton.
Re: Typed Lisp, A Primer (2019)
#16I've been thinking about typed lisp a bit lately since I started messing with CL again, and I admit the point about lists as code hadn't crossed my mind as something you have to deal with for any typing attempts. If you tried to make a "fully static typed lisp" likely you'd need a few holes for areas like that where they don't make sense. Well that or do the shenanigans things like c# do for param arrays where it is…
holes in the Idris sense, as in this spec? https://www.type-driven.org.uk/edwinb/papers/impldtp.pdf
I haven't looked too closely at Idris, I'll have to read this. Thanks for pointing me at it as I've been thinking about language design a lot lately (though I have no ideas that would warrant actually implementing a programming language currently).
Re: Typed Lisp, A Primer (2019)
#17I have hacked off and on on this
https://github.com/paulhoule/ferocity
which lets you write extended Java in a lispy syntax. It generates stubs for the standard library and other packages you choose, unerasing types by putting them into method names. It works pretty well with IDEs but there are still problems w/ type erasure such that some kinds of type checking can't be done by the compiler working directly on the lispy Java, probably I wouldn't implement newer features such as pattern matching that are dependent on type inference to work, though lambda definitions are feasible if you give specific types.
The 'extended' bit was almost discovered instead of invented in that it is pretty obvious that you need quote and eval functions such that you can write lispy Java programs that manipulate Java expressions. Said expressions can be evaled at runtime with a primitive interpreter or incorporated into classes that are compiled w/ Javac. The motivation of the thing was to demonstrate Java-embedded-in-Java (an ugly kind of homoiconicity) and implement syntactic macros from Java which I think that prototype proves is possible but there is a lot more to be done on it to be really useful. Enough has been implemented in it right now in that you can use it to write the code generator that builds stubs. It might be good for balls-to-the-walls metaprogramming in Java but I think many will think it combines all the worse features of Java and Lisp.
Re: Typed Lisp, A Primer (2019)
#18Yes. With macros and runtime logic it's possible to implement just about any type system in Lisp, even an ML-like system. Box everything and use macros to transparently pick it apart and reconstruct your wrapped type objects when you use them. My initial reaction to that whole idea was horror. The inefficiency! But maybe not necessarily. A compiler that understood the type system used, could optimize most of it away.…
Typed Racket is an example of a typed language built off of a dynamic base that still manages to use type information for optimization. The main way it does that is by using existing unsafe APIs from the dynamic language, but in a safe way with the type information.
Re: Typed Lisp, A Primer (2019)
#19> Augment Lisp with functional Haskell-like type declarations ;-) Since the article's publication, this is now possible with the industrial-grade Coalton: https://github.com/coalton-lang/coalton/
What I immediately thought of. Coal ton is a pretty awesome project
Re: Typed Lisp, A Primer (2019)
#20Earlier quoted context omitted.
holes in the Idris sense, as in this spec? https://www.type-driven.org.uk/edwinb/papers/impldtp.pdf
I haven't looked too closely at Idris, I'll have to read this. Thanks for pointing me at it as I've been thinking about language design a lot lately (though I have no ideas that would warrant actually implementing a programming language currently).
if i may suggest, as we seem probably similarly thoughtful about language design, and having been a Scheme person long ago, Python of course, optimizing compilers galore, etc. ... I find F# very neat, as it's essentially a Microsoft .Net runtime Ocaml, and is therefore (not syntactically, but semantically) reminiscent of Scheme/Lisp.