jbgi · June 5, 2025 14:44 · Jun 18, 2018 · Jun 18, 2018 · Jun 18, 2018 · Jun 18, 2018
diff --git a/Parametricity.md b/Parametricity.md
@@ -22,7 +22,7 @@ data Nu a where
 ```
 a `Nu` value could be constructed using some secret value inside type `s` and then be passed to un-trusted code without that code being able to read any `s` value (because `s` would be existentially quantified).
 
-4. Another judicious use of parametricity is the extra type variable used by the State Monad in haskell, that permit thread-safety and purity of mutating code, without requiring substructural types.
+4. Another judicious use of parametricity is the extra type variable used by the `ST` Monad in haskell, that permit thread-safety and purity of mutating code, without requiring substructural types.
 
 5. Just an extra type parameter and a `map` method is often very useful even in business code [1] and in so many other use cases [2] ...
 

diff --git a/Parametricity.md b/Parametricity.md
@@ -32,6 +32,8 @@ Probably because of the object-oriented tradition of using inheritance as the go
 but also for less obvious reasons, that are rooted into the design of the programming languages:
  - for programmers used to Java (and similar) it is often the framework of universal equality that is a blocking progress toward parametricity [4].
  - for C# programmers, reified generics add an additional barrier to understanding the value of parametricity [5].
+
+ So if you are a user of above languages and you want to make full use of parametricity: please ignore universal equality and reified generics! (and of course, type-casing/casting, runtime reflection, `null`, unchecked exceptions, etc.)
 
 [1] https://typelevel.org/blog/2015/09/21/change-values.html
 [2] http://newartisans.com/2018/04/win-for-recursion-schemes/

diff --git a/Parametricity.md b/Parametricity.md
@@ -5,9 +5,10 @@ I started to use generics in Java to improve reuse of the libraries I wrote at w
 but as I was growing a better understanding of types, parametricity and theorems for free,
 other compelling reasons became prominent:
 
-1. the free theorems help me know what a function can do and cannot do, base on its type signature only.
-Eg. given an unconstrained type variable, any value of this type that appears on positive positions (output)
-must comes from a value in negative position (imput), ie. the function cannot "invent" values of this type.
+1. the free theorems help me reason about code: given parametricity, I know what a function can do and cannot do,
+based only on its type signature.
+Eg. given an unconstrained type variable, any value of this type that appears in positive position (output)
+must come from a value in negative position (input), ie. the function cannot "invent" values of this type.
 
 2. increasing the parametricity of a method means less possible implementations hence less room for bugs
 (eg. as we all know, `forall a. a->a` has only one possible non-bottom implementation).

diff --git a/Parametricity.md b/Parametricity.md
@@ -5,9 +5,9 @@ I started to use generics in Java to improve reuse of the libraries I wrote at w
 but as I was growing a better understanding of types, parametricity and theorems for free,
 other compelling reasons became prominent:
 
-1. the free theorems give help me known what a function do an cannot do, base on its type signature only.
-Eg. given a unconstrained type variable, all value of this type that appears on positive positions (output)
-must come from values in negative position (imput), ie. the function cannot "invent" values of this type.
+1. the free theorems help me know what a function can do and cannot do, base on its type signature only.
+Eg. given an unconstrained type variable, any value of this type that appears on positive positions (output)
+must comes from a value in negative position (imput), ie. the function cannot "invent" values of this type.
 
 2. increasing the parametricity of a method means less possible implementations hence less room for bugs
 (eg. as we all know, `forall a. a->a` has only one possible non-bottom implementation).

diff --git a/Parametricity.md b/Parametricity.md
@@ -3,7 +3,7 @@ and that I am confident of being able to efficiently explain my code to co-worke
 
 I started to use generics in Java to improve reuse of the libraries I wrote at work,
 but as I was growing a better understanding of types, parametricity and theorems for free,
-two other compelling reasons became prominent:
+other compelling reasons became prominent:
 
 1. the free theorems give help me known what a function do an cannot do, base on its type signature only.
 Eg. given a unconstrained type variable, all value of this type that appears on positive positions (output)

diff --git a/Parametricity.md b/Parametricity.md
@@ -0,0 +1,39 @@
+I try to write code that is "maximally polymorphic" to the extent that I am sufficiently familiar with the concepts involved
+and that I am confident of being able to efficiently explain my code to co-workers if needed.
+
+I started to use generics in Java to improve reuse of the libraries I wrote at work,
+but as I was growing a better understanding of types, parametricity and theorems for free,
+two other compelling reasons became prominent:
+
+1. the free theorems give help me known what a function do an cannot do, base on its type signature only.
+Eg. given a unconstrained type variable, all value of this type that appears on positive positions (output)
+must come from values in negative position (imput), ie. the function cannot "invent" values of this type.
+
+2. increasing the parametricity of a method means less possible implementations hence less room for bugs
+(eg. as we all know, `forall a. a->a` has only one possible non-bottom implementation).
+
+3. judicious use of parametricity can help ensure critical security properties(assuming safe, pure, strongly typed language).
+Eg. universally quantification ensure that some un-trusted piece of code can be executed without fear that it could read some secret values.
+For example, given the type:
+```haskell
+data Nu a where
+  Unfold :: forall a s. (s -> Maybe (s, a)) -> s -> Nu a
+```
+a `Nu` value could be constructed using some secret value inside type `s` and then be passed to un-trusted code without that code being able to read any `s` value (because `s` would be existentially quantified).
+
+4. Another judicious use of parametricity is the extra type variable used by the State Monad in haskell, that permit thread-safety and purity of mutating code, without requiring substructural types.
+
+5. Just an extra type parameter and a `map` method is often very useful even in business code [1] and in so many other use cases [2] ...
+
+Parametricity is very much underused by developers of mainstream programming languages.
+I experimented that even experienced programmers strugle to see the point of parametricity [3].
+Probably because of the object-oriented tradition of using inheritance as the go-to tool for abstraction,
+but also for less obvious reasons, that are rooted into the design of the programming languages:
+ - for programmers used to Java (and similar) it is often the framework of universal equality that is a blocking progress toward parametricity [4].
+ - for C# programmers, reified generics add an additional barrier to understanding the value of parametricity [5].
+
+[1] https://typelevel.org/blog/2015/09/21/change-values.html
+[2] http://newartisans.com/2018/04/win-for-recursion-schemes/
+[3] https://twitter.com/gregyoung/status/769558636796358656
+[4] https://twitter.com/jb9i/status/776114745258741761
+[5] https://twitter.com/jb9i/status/842748586882404353