5 ms·

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 some

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.

throwaway17_17 4y ago
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 4y ago
  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 4y ago
    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 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/S0304397500000530/pdf?md5=30c03faf3942c17373ac0dcbb708ee7c&pid=1-s2.0-S0304397500000530-main.pdf 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 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 https://lfmtp.org/workshops/2017/inc/slides/murase.pdf (slides from a talk)
thesz 4y ago
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 4y ago
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 4y ago
  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.
jjtheblunt 4y ago
holes in the Idris sense, as in this spec? https://www.type-driven.org.uk/edwinb/papers/impldtp.pdf https://www.type-driven.org.uk/edwinb/papers/impldtp.pdf
- runevault 4y ago
  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 4y ago
    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 4y ago
      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 4y ago
        we are evidently clones
        runevault 4y ago
        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.

throwaway17_17 4y ago

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 4y ago
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 4y ago
  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 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/S0304397500000530/pdf?md5=30c03faf3942c17373ac0dcbb708ee7c&pid=1-s2.0-S0304397500000530-main.pdf 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 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 https://lfmtp.org/workshops/2017/inc/slides/murase.pdf (slides from a talk)

thesz 4y ago

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 4y ago

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 4y ago
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.

jjtheblunt 4y ago

holes in the Idris sense, as in this spec? https://www.type-driven.org.uk/edwinb/papers/impldtp.pdf https://www.type-driven.org.uk/edwinb/papers/impldtp.pdf

runevault 4y ago
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 4y ago
  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 4y ago
    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 4y ago
      we are evidently clones
      - runevault 4y ago
        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.