nelan@enuxha.eas.asu.edu (George Nelan) (08/07/90)
Howdy, Here's the scenario: I'm using ("real") Haskell to describe a program transformation algorithm. A program is represented as a set of data/type declarations that conveys somewhat more than what might be considered a "normal" amount of information about a program -- more or less corresponding to a direct encoding of semantic annotations. For instance, I define an expression to be: data Exp = BE BExp | AE AExp data BExp = ... -- basic expressions data AExp = WAE WAExp | SAE App -- applicative expressions data WAExp = ... -- a particular kind of AE type App = (Idn, [Exp]) -- a (raw) application And so on... The general idea is that various functions of the alg. transform *subdomains* - in the sense that inputs/outputs might be constrained to "subsets" of Exp. For instance, f1 might have both WAE & SAE AExp's as input but only WAE AExp's as output -- which is input to f2; etc. I can think of no convenient way to explicitly indicate (in Haskell) such notions. I consider it too painful to explicitly describe all the possible restricted subdomains as discreet data/type declarations (one runs out of constructor names too quickly amongst other things). In order to reason about things (usually via structural induction), it is then necessary to "go outside the metalanguage (Haskell)"; i.e., by introducing external Lemmata/Theorems. I find this annoying, inasmuch as it *seems* possible (in principle, anyway) to "prove" many things about correctness within the structure of the metalanguage (Haskell) itself. I would be interested in any useful suggestions on two levels: 1) - how to deal with this within the framework of Haskell/Hindley-Milner 2) - any other related ideas Note - no need to repeat the concepts of recent similar threads in c.l.f. Hey, go ahead; make my day: post it! -- George Nelan, ERC 252, Arizona State University, Tempe, Arizona, USA, 85287 INET: nelan@enuxha.eas.asu.edu UUCP: ...{allegra,{ames,husc6,rutgers}!ncar}!noao!asuvax!nelan QOTD: ever where ever = "what" : ever