[HN Gopher] Typed Lisp, A Primer (2019)
___________________________________________________________________
Typed Lisp, A Primer (2019)
Author : tagfowufe
Score : 64 points
Date : 2023-01-31 13:20 UTC (9 hours ago)
(HTM) web link (alhassy.com)
(TXT) w3m dump (alhassy.com)
| TOGoS wrote:
| > type's have always been there
|
| As have excessive apostrophe's.
| tmtvl wrote:
| Yes, unfortunately the article has a few spelling errors, it's
| still interesting though.
| dang wrote:
| Related:
|
| _Typed Lisp, a Primer (2019)_ -
| https://news.ycombinator.com/item?id=23878612 - July 2020 (26
| comments)
| neilv wrote:
| The Racket platform has Typed Racket, by Sam Tobin-Hochstadt, et
| al.
|
| https://docs.racket-lang.org/ts-guide/beginning.html
| vindarel wrote:
| > 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/
| runevault wrote:
| Oh hey I'll have to look at this at some point, luckily I'm
| already using SBCL for my re-learning.
| strawhatguy wrote:
| What I immediately thought of. Coal ton is a pretty awesome
| project
| wk_end wrote:
| Is Coalton industrial-grade? What does that mean? Is it used in
| industry?
|
| I'll note that the GitHub README says:
|
| > Coalton has not reached "1.0" yet. This means that, from time
| to time, you may have a substandard user experience.
| vindarel wrote:
| Yes, they use it for their quantum compiler, at HRL
| Laboratories (it was maybe initiated even at Rigetti).
| https://github.com/quil-lang/quilc
| Pet_Ant wrote:
| There is a similar project for Clojure:
| https://github.com/typedclojure/typedclojure
| PaulHoule wrote:
| I 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.
| retrac wrote:
| Yes. 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.
| kazinator wrote:
| It exists. Qi, Coalton.
| slaymaker1907 wrote:
| 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.
| aidenn0 wrote:
| With the disclaimer that cl:satisfies makes the tun-time type-
| system turing complete (and no implementation I know of chacks
| cl:satisfies at compile time), the compiler-available types are
| strictly non-recursive.
|
| For example, you cannot define a type that means "A List of type
| X" because that requires recursion i.e. this is not allowed:
| (deftype typed-list (x) `(cons ,x (or (typed-list ,x) null)))
|
| So one must either declare the type of the loop-local variable(s)
| (when iterating) or the first N item(s) of a list (when
| recursing), which is a bit unfortunate. SBCL, in particular, does
| a great job of inferring types at compile time with just a few
| annotations, but code that is optimizer-friendly is made
| significantly more ugly by this. Or, you know, people just end up
| using arrays for everything.
| shadowgovt wrote:
| Article makes one error that is mostly correct but can trip
| someone up in corner cases. In section 2.5, article makes the
| assertion `(the t e) [?] (or (check-type e t) e)`
|
| This may be true in some implementations, but the actual
| defintion of the `(the)` special operator is that if e is not
| type t, the behavior of `(the t e)` is undefined! Crashing when
| the type is determined to mismatch is one allowed result, but
| `the` is also the language's "escape hatch" to permit
| implementations to improve performance by throwing away runtime
| type information, at which point abusing types will crash in
| surprising ways.
| runevault wrote:
| I'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 just an array of objects.
|
| Mind you I feel like over time we are seeing dynamic and static
| typing converging more and more. Python type annotations are a
| thing to some degree I know, while c# a while back added the
| dynamic type.
| jjtheblunt wrote:
| holes in the Idris sense, as in this spec?
|
| https://www.type-driven.org.uk/edwinb/papers/impldtp.pdf
| runevault wrote:
| 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).
| jjtheblunt wrote:
| 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.
| runevault wrote:
| I am in fact dabbling in f# of late haha (My day job life
| is C# and f# does a lot of things well). I just never
| seem able to only mess with one thing so I'm also doing
| CL.
| jjtheblunt wrote:
| we are evidently clones
| runevault wrote:
| Haha.
|
| Out of curiosity have you seen the youtube channel Fast
| f#? He's doing a good job of talking about f# at several
| levels from simple to deep optimization work.
| jjtheblunt wrote:
| haven't seen that; thanks for the reference. i've been
| using the Microsoft dev docs, and fsharpforfunandprofit
| ... (and just situational awareness from an optimizing
| compilers background)
| thesz wrote:
| One can have types for lists as if they are constructed for
| code and for data. If type is valid for code, you can use it as
| code. If type is valid for data, you can use it as data.
|
| There should be no holes, but non-determinism.
| cjbgkagh wrote:
| AFAIK a hole is the usual term for the spot for a generic
| parameter. Sounds like you want a Top which the Any type.
| runevault wrote:
| To me there are two cases (and I could be wrong I'm only
| recently reading up on Category Theory and I'm not nearly as
| versed as I should be in PL theory). One for generics whether
| you generate different copies for each type (monomorphization
| I believe?) and other cases where that doesn't necessarily
| make sense, although maybe you could just use generics to
| handle the problem in question. Hm.
|
| I have to say I'm glad I started this thread because your
| reply and others have given me a lot to chew on.
| throwaway17_17 wrote:
| 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.
| runevault wrote:
| 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.
| throwaway17_17 wrote:
| 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/S03
| 0439750... (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)
___________________________________________________________________
(page generated 2023-01-31 23:01 UTC)