New answers tagged type-theory
3
In addition to András' answer, there's one thing you might want to be aware of with all this. I think it's not well known, because although I noticed it many years ago, I haven't really talked about it with many people.
Basically, if you think about some finite arithmetic behind the arithmetic of types, and compare it to some of the power series formula ...
3
Logarithm types are definitely a thing and have been noticed before by a number of people. In functional programming, a Type -> Type functor has a logarithm if it's representable, and then the logarithm is the representing object. See also this, this, and this. You are correct about the exponential functor being the bag functor, see e.g. this, where it's ...
4
The definition is not correct. It states that a machine is polynomial time (the field poly in poly-time-machine) when its running time is below the exponential function $n \mapsto 2^n$ (the definition is-poly). This would allow, for example, a running time $n \mapsto 1.5^n$, which isn not poly-time according to the accepted definition.
0
If you interpret a type $\tau$ as a set of values $Set_\tau$, then a natural definition for the interpretation of a polymorphic type would be the following:
$$Set_{\forall \alpha.\tau} = \bigcap_{\kappa \in Types} Set_{\tau[\alpha := \kappa]}$$
You need an intersection because intuitively a polymorphic type should work for all its instantiations.
Of course, ...
Top 50 recent answers are included
