Today I Learned (Not) Reflection

An intuition for reflection | QA9

This reflection is not the one for metaprogramming, but the property that if you fold a piece of data with its constructors, you get back the piece of data itself. In terms of list in Haskell, with constructors:

[] :: [a]
(:) :: a -> [a] -> [a]

and a folding function like this:

foldr :: (a -> b -> b) -> b -> [a] -> b

The property of reflection is then defined as this equation:

foldr (:) [] = id

Another "Today I Learned" quote:

It is known (although I am not sure where you can find this in a paper) that if you have parametricity and reflection, you can derive induction.

Especially revelatory quotes:

With induction, we are trying to summarize an infinite number of cases in some finite way. This finite way is with the constructors for the datatype.

not taking constructors and datatypes for granted, we might ask: but how do you know you correctly summarized that infinite set of values using your functions you call constructors

My intuition about reflection is that it contributes an essential property towards knowing you have the correct summary of your infinite set of data.

A philosophical quote:

All it does is go through the list and interpret cons as cons, nil as nil.

Data transformation is all about reinterpreting the constructors of data.