Am I right to think that value constructors are bijective functions?
2 Likes
Your intuitions are very well founded. But in general type constructors are not bijective. For example, the type constructor Just is injective (definitionally), but not surjective, since it maps no elements in its domain to Nothing. This is all a little weird because while types look like sets, and their constructors like functions, they aren’t quite like them either…
When you declare a type, you are declaring the inhabitants of that type (ignoring non-termination/bottom). This is kind of like surjectivity, because type constructors define the type. i.e. A type’s constructors are the only way to construct the type, so of course they look surjective.
In Haskell’s type system, the thing that makes type constructors look like bijection is that they are generative and injective (when something is both, it is known as matchable). Below, equality is considered in the type theoretic sense.
Generativity
For all f a == g b where f and g are generative, then f == g.
This is behind the notion of tagged unions (aka coproducts or sum types). If two values of a type are equal, then the type constructors used to create those values are the same. Again, this really is definitional, since two different type constructors do not map to the same term of a type.
Injective
For all f a == f b where f is injective, then a equals b.
For example, if you have Just a == Just b, then we know that a == b. This is also definitional, since type constructors are purely syntactic: a term in the target type is mapped uniquely onto by a value in the domain.
Matchability
Matchability is having both.
If you think about all this, these properties arise from the very definitions of type introduction in Haskell (and type theory in general). Having a type constructor that is not one of these two is non-sensical, and these properties are the reasons we can actually pattern match on the values of a type!
You can read more on page 58 of Richard Eisenberg’s thesis.
All this said, an example of a bijective type constructors would be any newtype, since they are nominal mappings over terms of types (e.g. newtype Foo = Foo Int; Foo is a bijective function from Int to Foo).
1 Like
Much appreciated for the clear and detailed response.
Here is a sense in which value constructors are bijective:
For each value t of type T there exists a unique way to construct that value, using the value constructors of T.
ie. all values of T can be constructed one and only one way using the value constructors of T.