@jesper @anuytstt I'm lost at this sentence in the introduction:
> For example the parametricity of a function f : A → B is a proof that f maps related inputs in A to related outputs in B, i.e. f is a morphism of reflexive graphs.
Which relations on A and B are we talking about?
Jaro Reinders
@jaror@social.edu.nl
PhD student at Delft University of Technology 🎓 in the @DelftPL group. Trying to build correct compilers from modular building blocks 🧩 in #Agda. I'm also a #Haskell enthusiast, #GHC contributor, and a member of the GHC Steering Committee and the Core Libraries Committee. Other than that I'd like to play some #folk guitar 🎶 and recently obtained a banjo 🪕. I also appreciate playing with language 📝 #lightverse.
social.edu.nl
Jaro Reinders
@jaror@social.edu.nl
PhD student at Delft University of Technology 🎓 in the @DelftPL group. Trying to build correct compilers from modular building blocks 🧩 in #Agda. I'm also a #Haskell enthusiast, #GHC contributor, and a member of the GHC Steering Committee and the Core Libraries Committee. Other than that I'd like to play some #folk guitar 🎶 and recently obtained a banjo 🪕. I also appreciate playing with language 📝 #lightverse.
social.edu.nl
@jaror@social.edu.nl
·
Dec 15, 2025
0
0
0
Loading comments...