Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

### martes 28 de octubre de 2008

11:00am Meeting room 302 (Mountain View), level 3

**Alvaro Garcia***, PhD Student**, IMDEA Software Institute*

### Can type systems help to write programs in a more
atural way?

#### Abstract:

Church numerals are a functional encoding of natural numbers. In the
pure (untyped) lambda calculus, the definition of certain operations
on Church numerals (addition, multiplication, etc) can be expressed
“naturally”, in the sense of easy-to-understand and re-use of
previously defined values. I’ve tried encoding these definitions in
Haskell but the Rank-n type system infers rather strange types for
numerals and operators. In his paper on System F, Reynolds suggested a
polymorphic type for Church numerals and for arithmetic
expressions. The way he defined them is not the same as the “natural”
one (which can be expressed in System F as well). I have found that it
can be expressed in Haskell (with some extra trickery) but it cannot
be expressed in Agda (due to restrictions on impredicativity). I
wonder if there is a type more general than Reynolds’ that is more
specific than the one inferred by Haskell’s.

I have an interest in how to express programs more “naturally” and on
the question of which features of the type system can help to achieve
that. I found Haskell’s Rank-n system and Agda’s predicativity a
hurdle for this case study. There are several proposals for making
type inference possible with less and less type annotations (MLF, HMF,
etc). For my PhD, I’m learning about types in programming and about
the role of type checking and type inference. I’m curious about the
limits of inference (not checking) and about the mechanisms that let
me express types and functions in a more “natural” way.