Post AqoPgpFCsneYWP7ZRI by aram@mastodon.sdf.org
 (DIR) More posts by aram@mastodon.sdf.org
 (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 #AqobiyHBTLiAYwpreq by burakemir@discuss.systems
       2025-02-05T17:27:53Z
       
       0 likes, 0 repeats
       
       @aram There are many ways to interpret "practical". One class of practical languages with limited use of System F translates code to an efficient lower level language and erases all types in the process. If you want something that preserves types at runtime, this strategy is not available.