[HN Gopher] Beyond inductive datatypes: exploring Self types
       ___________________________________________________________________
        
       Beyond inductive datatypes: exploring Self types
        
       Author : danny00
       Score  : 47 points
       Date   : 2021-10-30 15:39 UTC (7 hours ago)
        
 (HTM) web link (github.com)
 (TXT) w3m dump (github.com)
        
       | snugghash wrote:
       | I'm not in the field. For anyone else curious about relationship
       | to things like TLA+ (https://en.wikipedia.org/wiki/TLA%2B) - the
       | discussion at https://news.ycombinator.com/item?id=15583377 was
       | great.
        
       | the_french wrote:
       | This is an interesting idea but is there any description of the
       | soundness of this approach? Any functionality capable of
       | subsuming not just inductive types but higher-inductive types is
       | going to be _very_ subtle. I looked around on the repository but
       | I can 't find any formal description of the language or type
       | theory, which is worrying for a proof tool.
        
         | logicchains wrote:
         | There's a paper on the soundness of self types:
         | https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...
        
         | skybrian wrote:
         | The plan for Kind itself seems to be to allow possibly unsound
         | expressions (for example that don't terminate), but to have
         | consistency checkers. See:
         | 
         | https://github.com/kind-lang/Kind/blob/master/CONTRIBUTE.md#...
        
       ___________________________________________________________________
       (page generated 2021-10-30 23:00 UTC)