Do we Need Dependent Types? | Zendy

Daniel Fridlender | Zendy; Mia Indrika | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Do 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research