Twitter | Search | |
Brandon Williams
Subterranean homesick mathematician. Previously . Working on Available for hire:
6,749
Tweets
498
Following
3,635
Followers
Tweets
Brandon Williams 1h
Replying to @v_pradeilles
Yes exactly correct. Even the mere existence of `fatalError`, which is a function `() -> Never`, is proof of a false theorem. Anytime it is used you have gone outside the boundaries of Curry-Howard.
Reply Retweet Like
Brandon Williams 1h
Replying to @v_pradeilles
Yeah that is correct. You also cannot use `fatalError` in your implementation since then you can implement any function! The correspondence holds in an idealized programming language, which Swift is a close enough approximation to.
Reply Retweet Like
Brandon Williams retweeted
ジェシー 4h
TIL: Topology in Swift
Reply Retweet Like
Brandon Williams retweeted
John Carlos Baez Dec 9
Logic is all about what implies what... so it's fun to think about "implicational logic", where the only logical connective we get to use is "implies". Three axioms are all we need! Peirce's law is the spice in the pudding. (continued)
Reply Retweet Like
Brandon Williams 6h
Replying to @zats
Thanks for coming! Videos should be out today or tomorrow.
Reply Retweet Like
Brandon Williams retweeted
Chris Eidhof 11h
We (quietly) relaunched Swift Talk last week, and rewrote the backend from Rails to Swift. Without any performance tuning, it uses less than half the memory, and everything is much faster.
Reply Retweet Like
Brandon Williams retweeted
Sash Zats 8h
I was lucky enough to see Brandon presenting this as a talk @ NYC - great talk and a blog post - highly recommended in anticipation of the conference videos 🙂
Reply Retweet Like
Brandon Williams retweeted
Point-Free Dec 6
Point-Free throwback: Contravariance We explore the counterintuitive idea of contravariance, and how it is an indispensable tool for understanding composition. It has come up many times now, and we may not have noticed it unless we had studied it before.
Reply Retweet Like
Brandon Williams retweeted
Point-Free Dec 6
Replying to @pointfreeco
Most recently we saw that contravariance popped up out of nowhere in designing a snapshot testing library. This was very surprising, and gave us a wonderful way of transforming snapshot tests in ways that we would not have seen otherwise.
Reply Retweet Like
Brandon Williams Dec 6
Replying to @mdiep
Oh no. That’s a serious bummer and surprising.
Reply Retweet Like
Brandon Williams Dec 6
Replying to @mbrandonw
I’ve created a gist of the all the code in this article. Copy-and-paste it into a playground to poke around in a seemingly impossible Swift program 😃 (I recommend turning off automatic run)
Reply Retweet Like
Brandon Williams retweeted
Yasuhiro Inami Dec 5
This is a mind-blowing episode to watch... I mean, read.
Reply Retweet Like
Brandon Williams Dec 5
Replying to @SergDort
Yeah I can see that! A seemingly impossible surface! Similar to space filling curves, continuous everywhere but differentiable nowhere functions, etc...
Reply Retweet Like
Brandon Williams Dec 5
Replying to @tTikitu
I’ve got some references at the end of the article you might be interested in. In particular, there’s a set of slides with this one slide you might like:
Reply Retweet Like
Brandon Williams Dec 5
Replying to @tTikitu
Uh, well the predicates are on `BitSequence` right? For example `BitSequence.allSatisfy` answers whether or not a predicate holds on every value of `BitSequence`.
Reply Retweet Like
Brandon Williams Dec 5
Replying to @v_pradeilles
No you can’t implement arithmetic. For example, you can’t add anything to the bit sequence that returns 1 for every index.
Reply Retweet Like
Brandon Williams Dec 5
Replying to @v_pradeilles
Thanks! Nah that wouldn’t change its compactness. There are other ways to combine two bit sequences, we just can’t line them up one after the other. For example, we could interleave them so that even indices go to one and odd indices go to the other.
Reply Retweet Like
Brandon Williams Dec 5
Replying to @tTikitu
Oh no. Feel better!
Reply Retweet Like
Brandon Williams Dec 5
Replying to @DLX
And it’s precisely this compactness property that allows you to exhaustively search infinite sets by only searching a finite subset of them. That’s the rough idea at least.
Reply Retweet Like
Brandon Williams Dec 5
Replying to @DLX
BitSequence is compact because its points are clumped together in a particular way, and that gives it many finiteness properties. Int is not compact because it is infinite and discrete, and so its points are spread out.
Reply Retweet Like