#rust-internals

/

      • eddyb
        even if you overload them, let me infer the goddamn types mechanically instead of having to guess
      • cr1901: and what I got back was HoTT, which *not* what I was asking for
      • cr1901
        hmmm
      • eddyb
        HoTT isn't "signatures on arithmetic/algebras/etc."
      • HoTT is "almost all of math, in type theory instead of set theory"
      • like, machine-checkable proofs (you run a type-checker on your proof code, basically)
      • cr1901
        Maybe this will all make sense when I reread it "tomorrow"
      • eddyb
        funnily enough, HoTT is probably the first computationally-friendly formalism to handle real numbers "perfectly"
      • idk if anyone wrote a library for them
      • ekleog
        eddyb: hmm, random thought arising from previous discussion: exists T. T is just like !… is it?
      • eddyb
        cr1901: but like you could do calculus proofs, talking about small values, or rate of change or other funny things etc. and if you wanted to probably could build some vectors and tensors on top of that
      • cr1901: it's *extremely overkill* though
      • OmniMancer
        does type theory have an equivalent of the axiom of choice?
      • eddyb
        I don't regret it, but I still don't understand quantum physics
      • OmniMancer: HoTT specifically... disallows it? I forget
      • lemme Ctrl+F the book
      • cr1901
        eddyb: Yes, you mentioned something along those lines on Twitter
      • eddyb
        cr1901: heh
      • cr1901: anyway, I just found it funny that you had the same issue :P
      • cr1901
        I don't see myself going down that same path though
      • eddyb
        in type theory, something you might want to prove has a type, and the proof is constructing a value of that type
      • OmniMancer
        So not ZF rather than ZFC then?
      • eddyb
        "As with LEM, the equivalent forms (3.8.1) and (3.8.3) are not a consequence of our basic type theory, but they may consistently be assumed as axioms."
      • hmm
      • I know there are some set theory things that are just nonsense under type theory
      • well, constructivist type theory
      • because they're useless computationally
      • OmniMancer
        well the axiom of choice is more about being able to make choices from sets of infinite cardinality AFIAK
      • eddyb
        (I love it when theory meets reality :D)
      • OmniMancer: yes which is undecideable AFAIK
      • OmniMancer
        infinite things don't tend to be computable do they?
      • eddyb
        type theory can talk about infinite things
      • without being able to choose
      • OmniMancer
        indeed
      • No making copies of spheres with HoTT then :P
      • eddyb
        OmniMancer: some of these things you can prove, but only by "truncation"
      • as in, you can prove that there exists a proof
      • but to actually have the proof value would mean you have that vlaue
      • OmniMancer
        ah
      • eddyb
        like, `exists X. Y<X>` in type theory is roughly `(X: Type, Y<X>)`. it's a pair where the second element can refer to the first one. so for there to exist, you must at some point have known it
      • this is why it's "constructivist"
      • "to prove there exists it's sufficient to find one value" etc.
      • OmniMancer: "The axiom of choice, if we assume it, says that this is true for sets; as we will see below, it fails in general."
      • where "sets" here refers to certain types, not all types are set-like
      • "The truncation in the domain means we assume that for every x there exists some a : A(x) such that P(x, a), but that these values are not chosen or specified in any known way. The truncation in the codomain means we conclude that there exists some function g, but this function is not determined or specified in any known way."
      • OmniMancer: LEM is even funnier
      • OmniMancer: LEM is X | !X right?
      • OmniMancer
        ah yes, that one
      • eddyb
        in type theory, this is (in Rust syntax), `Result<X, fn(X) -> !>`
      • as in, you either get a value of type X or a way to turn a value of type X into UB (which how you do `!X` in type theory)
      • s/UB/anything else
      • but if you can't prove either `X` or `!X` separately... you can't make this sum type
      • *make a value of this sum type
      • OmniMancer
        indeed
      • eddyb
        so LEM in type theory would give you a proof oracle which would be... amazing :P
      • it's also impossible, computationally-speaking
      • OmniMancer: but if you "truncate" it (as in, it becoming "() if it has any possible values, or ! otherwise", with 0 data content either way), then that's fine because it doesn't actually contain either proof
      • so you can recover "proof-irrelevance" or w/e
      • OmniMancer
        ah
      • I find it interesting that for cryptography vulnerabilities the way the word oracle is used is somewhat misleading to what it actually represents in practice
      • eddyb
        haha
      • anyway, you want to avoid truncation because computational proofs are just... easier to motivate trusting, I guess
      • you can dump out the proof term as a huge value
      • because that's what it is
      • a finite value, or equation if you will
      • OmniMancer
        That reminds me of the Gödel incompleteness theorem
      • eddyb
        idk how related it is to Rusell's paradox, but type theory has an universe hierarchy for this
      • where only types in higher-up universes can talk in certain ways about types in lower-down universes
      • and the bad cases require an infinite stack of universes, instead of staying within a single general universe
      • OmniMancer: as in, typeof(()) = Type, typeof(Type) = Type1, typeof(Type1) = Type2, ...
      • errr I meant the type () not the value () in the first one
      • that might be confusing :P
      • should've said Nat or something
      • Raychen1 joined the channel
      • Raychen1 is now known as
      • cswindle has quit
      • cswindle joined the channel
      • OmniMancer
        is the Type () the type of the value ()?
      • munksgaard
        I'm getting this error whenever I try to run `./x.py <anything>` on a freshly created virtual machine. Any idea what's gone wrong? https://pastebin.com/4MAGYRXJ
      • cswindle has quit
      • mceier
        munksgaard: do you have curl installed (just a guess) ?
      • munksgaard
        mceier: I did not. It seems to work now, thanks.
      • Raychen1 joined the channel
      • Raychen1 is now known as
      • Raychen joined the channel
      • inad923 joined the channel
      • psychoslave has quit