O Hai

Plot twist indeed

...

Interesting! What is it? That old Syrian instrument, what’s it called, Lut?

It's an archlute, a western adaptation of the 17th century. The lute came into Europe somewhere around 700, mostly through the Arabs in Southern Italy and Spain.

Funny, I went to a lute concert last month by accident – I didn’t know what I was getting into and then this guy started taking a seat on stage and played songs about the Euphrates, and told stories about how Flamenco was heavily influenced by Arabian music.

>left physics for computer science

Well, I graduated, and took a job that I quite enjoy. During my studies I used a lot of C++ and Mathematica (was one of the founders of mathematica.stackexchange.com) so I knew a bit about programming, then got hooked on Haskell and from there it was a slippery slope to learning about type theory on the theoretical, and compilers on the practical side. I’ve got a very nice job working on a compiler nowadays, so I’d say it paid off. High energy particle physics jobs are fairly rare on the free market ;-)

whatever you say code monkey

We homotopies now.

I studied the then-version of the book a few years ago, when a release had just came out. What has changed since then? What new developments have I missed?

why should i care about anything homotopy, are there any useful results you could explain to a 12 year old or is this just pure autism as usual

git diff :-P
All I know about HoTT is from the book, I’m not following current research on the topic. It’s just a hobby. But I’ve heard people talk about it on conferences a couple of times, typically with a doubting »I don’t think this is worth it« mindset.

At 12 we learn things like [math](a+b)^2 = a^2+2ab+b^2[/math], I don’t think that’s a good age to measure human achievement by.

thought so

Well, there’s only so much you can do in life, and mathematics is a fairly lonely hobby. I found it very surprising how much of a time vs money trade getting a job was – I thought I spent a lot of time studying/working at uni, but boy is it different compared to a daytime job.

If you’re more knowledgeable, I’ve got a question (normal MLTT): an existentially quantified type can fairly easily be translated to a universally quantified one, [eqn]\sum_{x:A}P(x) = \prod_{y:B}\left(\prod_{x:A} \bigl(x,P(x) \bigr)\rightarrow y)\right) \rightarrow y[/eqn] – is the reverse possible as well somehow? I couldn’t come up with a proof in Agda, but also not a proof of its impossibility :-( (Let’s see how my Latex skills are holding up, fingers crossed…)

Got eeeeeem, epic troll xD

>was one of the founders of mathematica.stackexchange.com
Thank you for your service.

You’re welcome! I learned quite a bit just hanging around there, and even got a free T-Shirt. Hooray! I wear it when bouldering mostly, gotta bring the math to the mountains ;-)

That proposition doesn't make sense to me. Can you explain it? (Is y even a proposition?)

Hacked together on the fly in a tiny textbox. Pic related, a proper version of it, captured from the HoTT intro section.
The general idea is that an existential type can be encoded using only universal quantifiers (as a rank-2 type). My question would now be whether we can somehow use existential quantifiers to encode an existential, going the other way round.
Application: Haskell only has universally quantified types (and rank-N with a language extension), allowing us to express existentials in it. Would it be possible to have a (granted, very esoteric) type system with only existentials that would be just as powerful?

Hah!

Hey man, long time no see.

For better or worse, I never really stopped shitposting on Veeky Forums. During that time when I was around the corner form you in Germany, I also got into HoTT a little bit and last year eventually started doing youtube videos on dependent type theory, although it diverged into a smart contract programming series and now I'm waving back into math. Those things can be combined though, e.g. in
youtu.be/T9z3YQkKCLo
And I never stopped following Schreiber at the nLab who does physics in categories that are models for HoTT etc.
youtu.be/_O41kh0z_UM
I remember teaching you hom-functors with paint drawings :D Good you know more than me now.
in any case, one may move from one institution and faculty to the other, but I consider the distrinction between physics, math and computer science merely a social seperation of academics, and not a line you could evend draw throught the subject themselves. Best be looking at what all of those have to offer and do your own thing in the middle.

I was thinking about doing a light Curry-Howard shilling clip on the weekend..

Ha wow, nice to hear from you again! Did you stay in academia then?

> I remember teaching you hom-functors with paint drawings :D Good you know more than me now.
Ummm I forgot most of it again ;-)

No I didn't, I work in Augmented Reality now. Pretty cash.

Also, if you're interested I incidentally wanted to start working on a Haskell compiler project that would result in a $60,000 price money. As an expert, you'd do end up doing much more coding than I in the end, but if you're interested agreeing to $30,000 too, I have a job :)

I wrote an interpreter for the STG if that counts. And readlng the GRIN paper has been on my list for a while…
I’m a bit short on time these days though, sports and thinking pretty much switched roles in my life.
What’s that compiler project about?

Nevermind if you're not hungry.

What's STG?

Is this GRIN?
citeseerx.ist.psu.edu/viewdoc/download;jsessionid=E41D44B622B33450A3F06F547B1E61C2?doi=10.1.1.27.3918&rep=rep1&type=pdf

STG is the abstract machine that runs Haskell in GHC, in a nutshell. It’s what has an explicit stack and heap, and proper operational semantics. The readme on Github (»STGi« it’s called) is a bit more precise.

That link looks about right!

Gotta go now, train is arriving, visiting parents etc :-) You’ll find my real email I’m sure. Have a nice evening! (And everyone else as well.)

Newfag here who dis

Sup, I am (was) a tripfag back in the days when Veeky Forums was founded, around 2010/11/12, when I was finishing my Bachelor’s in (experimental) physics, before doing a master’s in theoretical physics. I talked a lot about math and relativity and the quantum world around here, but then lost interest and didn’t come here until now, when I realized I still had my tripcode lying around. And, to my surprise, googling my name with Veeky Forums actually turned up some results.

Back then this board was quite active (no idea how it’s nowadays), people were sometimes discussing proper science, but other than that it was the usual Veeky Forums shitshow. ICP brought up their »fuckin magnets how do they work« song so Veeky Forums was flooded with memes, [math]0.999\ldots\neq1[/math] trolls posted hourly, we had lots of infinite forces hitting walls of diamond, and we found out that [math]E=c[/math] thanks to Dr. Werner (»homeopathy with Dr. Werner« on Youtube).

Other tripfags I remember were Physics Guy, at the time doing a PhD I believe at CERN, and Harriet/EK which were desparate for attention without knowing shit about anything science, and being fully aware of that.

Oh, and the Emma Stone guy from above was also around during those days, except it seems he never left. :-)

There's a poster now who does topological quantum field theory and posts Yukari (from Touhou) a lot. Maybe you two can duke it out.

I miss the 0.999 threads.

Still pretty active. Main difference is that instead of meme shitposting we have /pol/ shitposting. Oh and we two have new schizophrenic attention whores.

They still happen quite often, idiot.

No they don't.

warosu.org/sci/?task=search&ghost=yes&search_text=999

big shitposting memes these days are flat earth and racial iq (and iq in general)

lol

Forgot I had these trips, this is fun.

[math]\begin{align*} A = \begin{pmatrix} a & a & a & a & a & a & a & a & a & a & \\ a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\\end{pmatrix} \end{align*} [/math]

Oh, I see! That makes sense. Apparently I'm rustier than I thought.

>Would it be possible to have a (granted, very esoteric) type system with only existentials that would be just as powerful?
That depends on what other primitive type operators you allow, I think. Are there simply-typed functions? Without them, you have a hard type even expressing a sum type, as a sum type has a parameter of type (A -> Type). What else might you consider as valid primitive types, if not product types?

Hmm, good point. I guess my mistake was that a [math]\Sigma[/math] type is not simply some »[math]\Sigma_{x:A}P x[/math]«, but rather the collection of how to create and annihilate values of that type, and for those we need dependent functions, and for those we need [math]\Pi[/math] types.
In other words, the question was probably wrong, but it took someone else to make me realize it. Thanks :-)

what do you have to say to this???:

youtube.com/watch?v=kxuU8jYkA1k

When I read the book some years ago I wondered about the minimal formulation of the dependent types formulation and ased a question here

cstheory.stackexchange.com/questions/27400/minimal-specification-of-martin-löf-type-theory

(cont.)

oh and I just remembered that at one point I wanted to write down the semantic/category theoretic dependent product definition more clearly than is done on the nLab, so I'm gonna post those two pages and maybe it helps.
I framed it in a very fibre bundle kind of way

start reading at the Discussion section, the abstract definition above can only make sense after

Oh wait, I even have notes on the product for a general dependent type theory, i.e. the characterization that you'd want.

My point is really that you can at least characterize his object without reference to the other. I doubt that in MLTT you can define the sum in terms of the product, but the characterization doesn't care anyway.
One softer variation of your question for me would then be: What do theories look like that only have one and not the other.

Granted, I never restricted myself in that way. My gripple with homotopy type theory etc. is that the fancy models of equality never seem to make for useable normal-adga like frameworks, do they?

Oh and one thing that seems to have changed totally in 2017 is the hardness of the image Captchas. It's super annoying. It comes down to making educated guesses of what the machine learning tool recognizes and what not