Coming from Haskell, Idris2 is an excellent programming language and experience.

kind of cool

Does Idris have types at runtime, or are they stripped out during compilation like with Haskell? Edit: 18:22 I get it.

Why is the type of Type, "Type 1", and not Type? =)

@yjlom

11 ай бұрын

Russell's paradox suppose we have access to the set of all sets, let's call it Set then we can construct a set Russell such that Russell = {x ∈ Set | x ∉ x} now consider the expression Russell ∈ Russell we can easily see that Russell ∈ Russell ⇔ Russell ∉ Russell let p ⇔ Russell ∈ Russell we can rewrite the above as p ⇔¬ p through the principle of the excluded middle, p ∨ ¬ p we can combine the two to have p ∧ ¬ p there are then techniques to use this to prove any arbitrary statement that can be solved either through dropping the principle of the excluded middle, severely limiting recursion, or preventing references to Set, the latter was chosen in Idris

@pmarreck

11 ай бұрын

@@yjlom But Russell's paradox only applies to Russell sets (the set of all sets that do not include themselves), not all sets (some of which can ostensibly include themselves); Russell sets are thus a subset of all sets. So why limit our modeling of sets to the Russell set, and not to all possible sets? Then we wouldn't have a paradox to violate, and a Type's type could be Type. ;)

@pmarreck

11 ай бұрын

@@yjlom I'm a "set neophyte" (and while a programmer, am a non-mathematician) so I looked further into this and it seems that most mathematicians have decided to base all of mathematics on ZFC set theory so I had no idea I was questioning some of the most basic assumptions in math LOL. Permitting "recursive sets" or let's say "Quine sets" (sets that can contain themselves) doesn't seem like it would affect THAT much mathematical theory though, it would simply need to be factored in when doing the accounting/theorizing, from what I can tell. I still maintain that there's no violation *in the functioning of the language* if the type of Type was Type, and that adhering to ZFC set theory in this case is an appeal to tradition fallacy. ;)

@yjlom

11 ай бұрын

@@pmarreck I'm also not a mathematician (as well as a pretty bad computer scientist), but I can see it thanks for digging into it!

@soracc_

8 ай бұрын

​@@pmarreck - No you cannot just have `Type : Type`, and there is violation in the functioning of (at least the Idris) language, for it's used as a proof assistant, which cannot allow leaky foundation. The foundation of Idris is not ZFC, but dependent type theory, which has its own version of RP. - Your assumption that it wouldn't affect much mathematics is also wrong. Russell's paradox is an example why/how "Quine sets" can't be (easily) accounted for, possibly contrary to your intuition (and that of many mathematicians before the time of rigourous foundation). Naive set theory is not called naive for no reason. People invented the now familiar formulation of ZFC (with axiom of regularity) to mitigate RP and friends. I think it's also important to notice that "sets that contain themselves" are not "banned", it's just consequence of the AoR (think the difference between not allowing pets and not allowing a female golden retriever in some cafe). - It's really not that you are questioning "assumptions" that based on belief, but results (or theorems) that are both mathematically and practically proven (of course, "prove" means something very different in these two contexts). I don't mean to put my words harshly, however, I think you are more "not understanding" than "questioning". If you are interested, google "Universe Levels, Agda" can lead you to the ways people deal with those paradoxes in a type based theory. Actually, you idea that is would be convenient for one to be able to "write" `Type : Type` in a program is not at all a bad one (again, see universe level in Agda). We just need to realise it's only a shorthand and not really what happens. I have to reiterate, it's never my intent to be overly critical, and if my tone is off, apologies in advance. If I made any factual mistake, please let me know as well.

Way too complicated for the audience, I assume. That there was no mention of the advantage of using linearity didn’t help.

@pmarreck

11 ай бұрын

It seems that it was assumed that one had familiarity with either Idris, Haskell or the Idris book. I started to get lost in the weeds around the middle, but I haven't finished making my way through the Manning book yet. I'll try to return to this after that