Open AccessDo we Need Dependent Types?
Author(s) -
Daniel Fridlender,
Mia Indrika
Publication year - 2001
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v8i10.20466
Subject(s) - haskell , arity , natural number , modulo , programming language , numeral system , type (biology) , computer science , arithmetic , mathematics , functional programming , combinatorics , discrete mathematics , biology , ecology
Inspired by [1], we describe a technique for defining, within the Hindley-Milner type system, some functions which seem to require a language with dependent types. We illustrate this by giving a general definition of zipWith for which the Haskell library provides a family of functions, each member of the family having a different type and arity. Our technique consists in introducing ad hoc codings for natural numbers which resemble numerals in lambda-calculus.