[charlieflowers]

What is the thought process behind him using the term "witness"? I can tell it is backed by an interesting perspective and I'd like to learn more about that perspective.

At one point, he said this witness "proved" something ... so is this coming from "propositions as types"?

[maxiepoo]

The use of the term "witness" here comes from constructive logic, where proofs of propositions have actual computational content. There "witness" means the same thing as "proof" but is more evocative that the proof is data that can actually be manipulated.

You might like this article if you're interested to learn more: http://jozefg.bitbucket.org/posts/2015-01-09-constructivism....

[charlieflowers]

Ah, I found it: https://wiki.haskell.org/Type_witness

In my own words, a "type witness" is a Haskell idiom (maybe broader?) that allows you to perform dynamic casts.

Here's the first example from that link:

A simple witness type might be defined over the Int, Bool and Char types like so:

data Witness a where IntWitness :: Witness Int BoolWitness :: Witness Bool CharWitness :: Witness Char

dynamicCast IntWitness IntWitness pa = Just pa

dynamicCast BoolWitness BoolWitness pa = Just pa

dynamicCast CharWitness CharWitness pa = Just pa

dynamicCast _ _ _ = Nothing