🚀 go-pugleaf

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