Lambda the Ultimate

I have been looking at and using programming languages for nearly 30 years now. I have just finished reading http://lambda-the-ultimate.org/node/100 and have found the various disussions "interesting". In terms of language design, I have looked at Chris Strachey and Robert milne's book "A Theory of Programming Language Semantics", Dana Scott's "Denottaional Semantics" and David Harland's "Polymorphic Programming Langugaes" and "Comcurrency and Programming Languages".

What I am interested in is the following question. In Static Type checking systems as well as Dynamic Type Checking systems, what is the effect of making Types (or Type Tags) first class citizens of the programming language? What is the effect of being able to create new types within the code, in other words having a function that on different invocations returns a new type? How does ST handle this (either theorectically or practically)?

Secondly, in ST languages, how is one able to create polymorphic structures without recource to "type variables"? Or another way to put it, how does St languages determine the type of a type variable?

I may not be grokking the way types are used in OCAML and CLEAN. An minor example of one problem I see with them is that I cannot (that I have yet found - if anyone knows how this would be achieved please let me know) create types that take any kind of value of any type.

Let me explain. I understand that it is easy to create a structure in these languages using "type variables". So I can create a list that can take any type of value, as long as all element values are the same type. What I want to do is create a list that has a variety of values of different types (simultaneosly) without having to create a union type. There are problems I have been involved in that required this kind of solution. Solutions developed ended up being far more complicated that the problem required because of static type checking available at the time.

[ 1 2.0 array.of.something "a atring" true ]

In OCAML the following creates a tree

type 'a btree = Empty | Node of 'a * 'a btree * 'a btree;;

My problem is that 'a sets all Nodes to have the same type for the datum values, where I really need the datum values to be of different types.

The requirement is that the code should not be required to be recompiled to add in an additional type signature for the structure. In other words, it needs to be future proof.

An area that I see types as being first class values is in a compiler. It has to be able to create new types on the fly and process them in the analysis of a programming language source file.

I have been working on a personal project of a new language that has types, code, processes, environments, etc as first class values - some of the facilities are to allow the creation of new code values (from within functions) and having functions defined as either lazy or eager. It purpose is to investigate abstraction. One area of abstraction is to see how to add code in the definition of a function that evaulates lazy parameters to give an eager parameter scheme.

Where I can use ideas from existing languages I will do so.