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

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