Lambda the Ultimate

I am interested in writing a compiler capable of doing whole-program monomorphization (similar to MLton) to allow for efficient data representations and other optimizations. However, I am also interested in supporting a number of features such as higher rank types, existential types (wrapped up via data constructors), user-definable kinds, and polymorphic recursion.

Since I'm only interested in being able to remove polymorphism over values, an obvious way of making this work would be to restrict things like polymorphic recursion to occurring over non-value-kinded types. Images of types, combined with explicit wrapping and unwrapping, would allow things like the usual typed interpreter example (pretend Haskell has user-definable kinds):

{-# LANGUAGE GADTs, EmptyDataDecls #-}

-- kind Image_Kind
data Int_Image  -- :: Image_Kind
data Bool_Image -- :: Image_Kind

data Image a where
  Image_Int  :: { int  :: Int  } -> Image Int_Image
  Image_Bool :: { bool :: Bool } -> Image Bool_Image

data Exp a where
  Val :: Image Int_Image -> Exp Int_Image
  Gt  :: Exp Int_Image -> Exp Int_Image -> Exp Bool_Image
  If  :: Exp Bool_Image -> Exp a -> Exp a -> Exp a

-- eval :: forall (a :: Image_Kind). Exp a -> Image a
eval :: Exp a -> Image a
eval (Val n)    = n
eval (Gt a b)   = Image_Bool (int (eval a) > int (eval b))
eval (If a b c) = if bool (eval a)
                    then eval b
                    else eval c

x :: Int
x = int $ eval (If (Gt (Val $ Image_Int 5)
                       (Val $ Image_Int 3))
                   (Val $ Image_Int 42)
                   (Val $ Image_Int 0))

Language support for getting "images" of types would make this less verbose.

Is there any prior work in this area? How far can you push the limits? Are there any clever compilation schemes for tagging values with appropriate size/type data for selecting amongst monomorphic functions at runtime (which is essentially what you're doing manually with Image_Int and Image_Bool)?

Robert DeLine, Gina Venolia, and Kael Rowan, "Software Development with Code Maps", Communications of the ACM, Vol. 53 No. 8, Pages 48-54, 10.1145/1787234.1787250

Getting lost in a large code base is altogether too easy. The code consists of many thousands of symbols, with few visual landmarks to guide the eye. As a developer navigates the code, she follows hyperlinks, such as jumping from a method caller to a callee, with no visual transition to show where the jump landed. ... Better support for code diagrams in the development environment could support code understanding and communication, and could serve as a "map" to help keep developers oriented. ... Our goal is to integrate maps into the development environment such that developers can carry out most tasks within the map.

Although the focus of this article is largely on "Code Map as UI", there are hints of the possibility that we might eventually see "Code Map as Language Element" (for example, the comment that "An important lesson from the Oahu research is that developers assign meaning to the spatial layout of the code. Code Canvas therefore takes a mixed initiative approach to layout. The user is able to place any box on the map through direct manipulation..."). The same ideas will of course be familiar to anyone who has worked with environments like Simulink, which provide a combination of diagrammatic structuring and textual definition of algorithms. But in the past such environments have only really been found in specific application domains -- control systems and signal processing in the case of Simulink -- while the Code Map idea seems targeted at more general-purpose software development. Is the complexity of large software systems pushing us towards a situation in which graphical structures like Code Maps will become a common part of the syntax of general-purpose programming languages?