类型为一等值的语言？

Question

有没有一种语言,它是:

1)功能性

2)有类型推断

3)已经cur.不安

4)并且具有类型作为一等值

也想从它编译到JVM和/或CLR

Answer 1

F#是功能性的,并且具有类型推断,currying和类型作为一流值,因为您可以通过反射在运行时剖析类型.它编译为CLR并在Mono上运行良好.

实例:从我的(非免费)第一条采取的结构打字在F#.NET杂志:

以下createType函数创建一个新的.NET程序集,新模块和给定名称的新公共类类型:

> 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

我刚开始学习它,但Coq可能适合你.

很可能有一个函数接受一个类型(是原始类型,而不是该类型的实例)并返回另一个类型(再次,只是类型,而不是实例).如果您对程序的正式验证感兴趣,那么值得一看.

它还有一个很好的好处,能够将它的代码转换为Haskell/OCaml/Scheme,这样你就可以使用他们的IO /库,因为Coq往往缺乏它们.

它具有类型推断和currying,但类型推断并不完美,因为语言的类型系统远远超出标准的Milner-Hindley类型系统(并且更具表现力).