Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Typed Lisp, A Primer (2019)

alhassy.com

Post reply on HN
Print view View original

21–30 of 31 posts

Re: Typed Lisp, A Primer (2019)

#23

Post by aidenn0 »

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.

Re: Typed Lisp, A Primer (2019)

#24

Post by runevault »

jjtheblunt wrote: post #20
runevault wrote: post #16

Earlier quoted context omitted.

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.

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.

Re: Typed Lisp, A Primer (2019)

#25

Post by jjtheblunt »

runevault wrote: post #24
jjtheblunt wrote: post #20

Earlier quoted context omitted.

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.

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.

we are evidently clones

Re: Typed Lisp, A Primer (2019)

#26

Post by wk_end »

vindarel wrote: post #4

> 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/

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.

Re: Typed Lisp, A Primer (2019)

#27

Post by shadowgovt »

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 τ e) ≈ (or (check-type e τ) e)`

This may be true in some implementations, but the actual defintion of the `(the)` special operator is that if e is not type τ, the behavior of `(the τ 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.

Re: Typed Lisp, A Primer (2019)

#28

Post by runevault »

cjbgkagh wrote: post #10
runevault wrote: post #3

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…

AFAIK a hole is the usual term for the spot for a generic parameter. Sounds like you want a Top which the Any type.

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.

Re: Typed Lisp, A Primer (2019)

#29

Post by runevault »

jjtheblunt wrote: post #25
runevault wrote: post #24

Earlier quoted context omitted.

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.

we are evidently clones

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.

Re: Typed Lisp, A Primer (2019)

#30

Post by jjtheblunt »

runevault wrote: post #29
jjtheblunt wrote: post #25

Earlier quoted context omitted.

we are evidently clones

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.

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)
Post reply on HN