jbgi/Parametricity.md

## Parametricity.md

      
    Raw
  

              Parametricity.md
            
          
    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,
other compelling reasons became prominent:


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.


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).


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:


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).


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.


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].

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/
[3] https://twitter.com/gregyoung/status/769558636796358656
[4] https://twitter.com/jb9i/status/776114745258741761
[5] https://twitter.com/jb9i/status/842748586882404353