[HN Gopher] Having your compile-time cake and eating it too
       ___________________________________________________________________
        
       Having your compile-time cake and eating it too
        
       Author : signa11
       Score  : 16 points
       Date   : 2025-05-25 10:54 UTC (1 days ago)
        
 (HTM) web link (0x44.xyz)
 (TXT) w3m dump (0x44.xyz)
        
       | aatd86 wrote:
       | Is it perhaps a eli5 way of speaking about higher kinded types
       | and type checking decidability?
       | 
       | Is it about types not being available in the frontend of the
       | language as first class values?
       | 
       | Or is it about types not being defined as set of values but
       | something else?
       | 
       | It got me a little confused so I am asking.
        
         | codethief wrote:
         | > It got me a little confused
         | 
         | Not only you! The post is all over the place...
        
         | codebje wrote:
         | It's a confusing (and confused) article. The parts on type
         | systems are expressing IMO a fair observation that dependent
         | types are weird and hard, but without any sense of
         | understanding what they are or what they can do that might
         | justify their cost.
         | 
         | The parts on compile time execution are the better parts of the
         | article, IMO. There's food for thought here. The author might
         | enjoy reading up on partial evaluation.
         | 
         | Then, fulfilling Greenspun's 10th, the article reinvents Lisp
         | macros.
        
       | burakemir wrote:
       | One angle (no static types) is racket, which knows multiple
       | stages for its macros. Maybe the most developed actually working
       | "new tradition".
       | 
       | Researchers have also looked into multistage programming, which
       | is enabled by representing code at runtime. Including how to
       | represent it in type systems/logic.
       | 
       | For Scala, there was a realization that both macros and
       | multistage programming need a representation of programs. I am
       | falling asleep so can't dig out references now, but it is
       | exciting stuff and I think the last word has not been written on
       | all this.
        
       ___________________________________________________________________
       (page generated 2025-05-26 23:01 UTC)