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:
“It is vain to expect virtue from women till they are, in some degree, independent of men ... Whilst they are absolutely dependent on their husbands they will be cunning, mean, and selfish, and the men who can be gratified by the fawning fondness of spaniel-like affection, have not much delicacy, for love is not to be bought, in any sense of the words, its silken wings are instantly shrivelled up when any thing beside a return in kind is sought.”
—Mary Wollstonecraft (1759–1797)
“The American man is a very simple and cheap mechanism. The American woman I find a complicated and expensive one. Contrasts of feminine types are possible. I am not absolutely sure that there is more than one American man.”
—Henry Brooks Adams (1838–1918)