[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)