Podcasts Technology Iowa Type Theory Commute Curry-style versus Church-style, and the nature of type annotations

Curry-style versus Church-style, and the nature of type annotations

Published: Jan. 30, 2020, 11 p.m.

b'

In Curry-style typing annotations -- for example, the types of bound variables -- are erased, and not truly (semantically) part of the term.\\xa0 In Church-style, they are intrinsic to the term and are truly there.\\xa0 Discussion of some of the practicalities of Curry-style typing, in particular type annotations versus proving typings.

'