Dependent Types
Epigram is essentially a typed lambda calculus with generalized algebraic data type extensions, except for two extensions. First, types are first-class entities, of type ; types are arbitrary expressions of type, and type equivalence is defined in terms of the types' normal forms. Second, it has a dependent function type; instead of, where is bound in to the value that the function's argument (of type ) eventually takes.
Full dependent types, as implemented in Epigram, are a powerful abstraction. (Unlike in Dependent ML, the value(s) depended upon may be of any valid type.) A sample of the new formal specification capabilities dependent types bring may be found in The Epigram Tutorial.
It is planned that the forthcoming version of Epigram, Epigram 2, will be based on Observational Type Theory, a new development of constructive type theory.
Read more about this topic: Epigram (programming Language)
Famous quotes containing the words dependent and/or types:
“For my part, I have no hesitation in saying that although the American woman never leaves her domestic sphere and is in some respects very dependent within it, nowhere does she enjoy a higher station . . . if anyone asks me what I think the chief cause of the extraordinary prosperity and growing power of this nation, I should answer that it is due to the superiority of their woman.”
—Alexis de Tocqueville (1805–1859)
“He’s one of those know-it-all types that, if you flatter the wig off him, he chatter like a goony bird at mating time.”
—Michael Blankfort. Lewis Milestone. Johnson (Reginald Gardner)