Language with types as first-class values?

Question

Is there a language, which is:

1) functional

2) has type inference

3) has currying

4) and has types as first-class values

also would like to compile from it to JVM and/or CLR

Answer 1

F# is functional and has type inference, currying and types as first-class values in the sense that you can dissect types at run-time via reflection. It compiles to the CLR and works well on Mono.

EXAMPLE: Taken from my (non-free) article Structural Typing in the F#.NET Journal:

The following createType function creates a new .NET assembly, new module and new public class type of the given name:

> let createType typeName =
    let name = System.Reflection.AssemblyName(Name="tmpAssembly")
    let run = System.Reflection.Emit.AssemblyBuilderAccess.Run
    let builder = System.Threading.Thread.GetDomain().DefineDynamicAssembly(name, run)
    let mdl = builder.DefineDynamicModule "tmpModule"
    let attrs = TypeAttributes.Public ||| TypeAttributes.Class
    mdl.DefineType(typeName, attrs);;
val createType : string -> TypeBuilder

Answer 2

I just started learning it but Coq might work for you.

It's quite possible to have a function which takes in a type (yes a raw type, not an instance of that type) and return another type (again, just the type, not an instance). If you're at all interested in formal verification of programs it's worth a look.

It also has the nice little benefit of being able to convert it's code to Haskell/OCaml/Scheme so that you can use their IO/Libraries since Coq tends lacks them.

It has type inference and currying but the type inference isn't perfect as the language's type system is well beyond (and more expressive than) a standard Milner-Hindley type system.