Posts by aram@mastodon.sdf.org
(DIR) Post #Ans193uczlquoDQJf6 by aram@mastodon.sdf.org
2024-11-09T15:21:32Z
0 likes, 0 repeats
If it's a unityped language, like Lisp, it's just a list, if it's a typed language, then it's an AST, etc. It could even be a dependently-typed AST, why not?
(DIR) Post #Ans1EmP10eV4EyMaAq by aram@mastodon.sdf.org
2024-11-09T15:23:37Z
0 likes, 0 repeats
When chosing whether to interpret codes as data or as programs, one simply controls beta reduction dynamically.
(DIR) Post #Ans1GYBgpbCWjUyUfw by aram@mastodon.sdf.org
2024-11-09T15:24:14Z
0 likes, 0 repeats
AFAICT this definition captures all languages commonly considered homoiconic, and rejects languages commonly not considered homoiconic. Is there a language for which this definition fails to capture its desired properties?
(DIR) Post #ApXP1MPZ6MlKKC9Yrg by aram@mastodon.sdf.org
2024-12-29T12:25:40Z
0 likes, 0 repeats
@amoroso I don't see it? Maybe it's not enabled for all users?
(DIR) Post #ApXP76ma7chbafeyAK by aram@mastodon.sdf.org
2024-12-29T12:26:40Z
0 likes, 0 repeats
@amoroso And by I don't see it, I mean I see the control characters.
(DIR) Post #Aq5QAsQdeajeLbDmd6 by aram@mastodon.sdf.org
2025-01-14T22:18:48Z
0 likes, 0 repeats
I believe β-reduction in interaction combinators is not monotonic with respect to partial evaluation. In other words only program reduction (no free variables) is β-optimal. Is this true?
(DIR) Post #Aq5QFpbvYfBB3VrdLc by aram@mastodon.sdf.org
2025-01-14T22:19:45Z
0 likes, 0 repeats
Proof 1: partial evaluation can reduce irrelevant redexes in subnets that would be erased in lazy evaluation for specific inputs.
(DIR) Post #Aq5QGx7X7eSYdWBLgu by aram@mastodon.sdf.org
2025-01-14T22:19:52Z
0 likes, 0 repeats
Partial reduction of lambda bodies is "pessimistic" in the sense that the partial reduction has to work for all inputs, whereas specific inputs can entail different dynamic behaviors in the reduction of a complete program.
(DIR) Post #Aq5QHGG1yHXvzNIu4e by aram@mastodon.sdf.org
2025-01-14T22:20:00Z
0 likes, 0 repeats
Partial evaluation seems to imply some degree of strictness and be at odds with lazy evaluation.
(DIR) Post #Aq5QItWrRk1O4oxGpU by aram@mastodon.sdf.org
2025-01-14T22:20:07Z
0 likes, 0 repeats
I have a specific counter example in mind but it's for a non-λ-calculus system. I don't know if inets guarantee β-optimality for all computational systems or just for λ-calculus.
(DIR) Post #Aq5QKnk3vwh8hw2Tmy by aram@mastodon.sdf.org
2025-01-14T22:20:39Z
0 likes, 0 repeats
Lazy evaluation means we compute only what we need, but with partial evaluation we don't know what we're going to need.
(DIR) Post #Aq5RcjWGTIQUmJhRLc by aram@mastodon.sdf.org
2025-01-14T22:34:52Z
0 likes, 0 repeats
I am implementing CUE on top of interaction nets.
(DIR) Post #AqoNVM2MvxqSqNWDr6 by aram@mastodon.sdf.org
2025-02-05T14:50:10Z
0 likes, 0 repeats
Few systems have been so thoroughly studied and yet so little implemented in practical programming languages as System F.
(DIR) Post #AqoNh2SzWTKRcbXhrs by aram@mastodon.sdf.org
2025-02-05T14:51:27Z
0 likes, 0 repeats
System F is extremely powerful, but it doesn't support type inference, hence languages converged around a Hindley-Milner type system, which is a restriction of System F.
(DIR) Post #AqoNoejddj6CKuxfLU by aram@mastodon.sdf.org
2025-02-05T14:52:03Z
0 likes, 0 repeats
HM is not powerful enough, so people bolted on various extensions (some that go beyond what's possible with System F) that preserve principal typing and type inference (although the lack of type annotations is somewhat of an illusion, as types themselves require special syntactic encodings which demand quite a lot of annotation, see ADTs vs. GADTs for example). Other factions simply required dependent types (because they were doing logic), so they were willing to give up full type inference.
(DIR) Post #AqoOZgFJq7TydJCcvg by aram@mastodon.sdf.org
2025-02-05T14:59:03Z
0 likes, 0 repeats
As such, today there are two camps, "simple" languages based off HM (with extensions) and full TI, and "complex" languages (usually based on dependent types) and limited TI.
(DIR) Post #AqoP150rrgRHGUVZmi by aram@mastodon.sdf.org
2025-02-05T15:07:19Z
0 likes, 0 repeats
An unexplored space in practical programming languages is System F itself. What if we had a practical programming language that just uses System F instead of HM with byzantine extensions? How would that look and feel like?
(DIR) Post #AqoPUa9z8jUYGPqBQO by aram@mastodon.sdf.org
2025-02-05T15:12:42Z
0 likes, 0 repeats
The effort done in the dependent type world shows that partial type inference is still very effective in practice, so perhaps we'd lose less than one expects. On the other hand we'd gain a lot of simplicity. System F is simple! Dare I say, it's simpler than HM, even.
(DIR) Post #AqoPgpFCsneYWP7ZRI by aram@mastodon.sdf.org
2025-02-05T15:14:28Z
0 likes, 0 repeats
Has there been any work in producing a language like this?
(DIR) Post #Aqr5We4a9DSJMxtpoW by aram@mastodon.sdf.org
2025-02-06T22:13:36Z
0 likes, 0 repeats
This instance sucks. What's a good, math/type-theory oriented Mastodon instance with good performance, high character limit, and LaTeX support?