[Haskell-cafe] Constructor discipline and dependent types.

Patrick Browne patrick.browne at dit.ie
Sun Jul 17 11:03:52 CEST 2011


Hi,
My understanding of the constructor discipline (CD) is that it is a
restriction on the form of an equation that guarantees that the equation
represents an executable function. The CD restricts the LHS of an
equation to consist of a function name, constructors, and variables.
Also there should be no new variables on the RHS.
So CD permits function to be defined and prohibits general assertions
which are more in the domain of a specification language.
Question 1: Is the above a reasonable understanding of CD?

Question 2: I have read that the lack of dependent types (DT) prevents
writing general assertions in Haskell. Is CD related to DT?  If so how
are they related?

Regards,
Pat

This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie



More information about the Haskell-Cafe mailing list