New answers tagged type-systems
3
$\newcommand{\Alg}{\mathsf{Alg}\ }$
$\newcommand{\NatF}{\mathsf{NatF}\ }$
$\newcommand{\Nat}{\mathsf{Nat}}$
$\newcommand{\map}{\mathrm{map}\ }$
$\newcommand{\Z}{\mathrm{Z}}$
$\newcommand{\S}{\mathrm{S}}$
I don't think this is an actual counter-example.
Parametricity implies:
$$∀(α : \Alg \NatF t) (g : r → t)(x : \NatF r). \\
α\ [r]\ g\ x = α\ [t]\ (λx.x)\ (\...
Top 50 recent answers are included
Related Tags
type-systems × 81type-theory × 42
pl.programming-languages × 24
lambda-calculus × 15
lo.logic × 13
dependent-type × 11
typed-lambda-calculus × 11
type-inference × 11
reference-request × 6
functional-programming × 5
calculus-of-constructions × 4
object-oriented × 4
ct.category-theory × 3
denotational-semantics × 3
haskell × 3
normalization × 3
operational-semantics × 3
coq × 2
compilers × 2
set-theory × 2
recursion × 2
linear-logic × 2
monad × 2
homotopy-type-theory × 2
parametricity × 2