Dependent Types and Parametric Polymorphic Types
I just ran across these notes Turing made in response to some communication from Max Newman:
See Ian Grant's Weather Report agosto 08, 2022 in particular the second part:
And there's some text to explain it: see https://prooftoys.org/ian-grant/hm/ in particular, page 7 of the tutorial:
See Archive Centre King's College.
I was triggered by thinking about the dependent Types in Idris: see Marco Perone - Fun With Categories.
Subscribe to Lambda World.
Comments
Post a Comment