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