榆树 - 检查值的类型

Question

是否存在检查Elm中变量类型的函数？例如(repl):

numberTwo = 2
.....
returnType numberTwo
"number" : String

这样做的动机是,当你使用Signal.map[n]这种情况时,通常会出现并不是所有要应用的函数的参数都是信号 - 它们通常必须被"提升"为信号使用Signal.constant- 如果我可以检查它的类型参数,我可以创建一个函数Signal.allSigMap[n],将这些参数自动转换为信号.

所以

Signal.map2 grandFatherClock clockSignalElement (Signal.constant cabinetElement)

变

Signal.allSigMap2 grandFatherClock clockSignalElement cabinetElement

可能是不好的做法.请告诉我.

Answer 1

我会首先回复你的意图,returnType作为一种促进类型的方式Signal.这将导致returnType沿途的某个或其他功能实际上返回一个类型而不是一个类型,String因为没有其他方法可以使类型检查器满意.

这样的功能不存在,并且不能像现在这样在Elm中存在.您要求的是能够检查值编译时间类型然后在该类型上运行函数的内容.

要了解为什么这与Elm中当前存在的任何东西完全不同,让我们假设存在这样的函数.

returnType : a -> ?

我们立刻遇到了第一个问题,即究竟是什么类型returnType.让我们手动这个并说我们有一个所谓的类型的类型Type(它有自己的一组逻辑问题,我们将把它放在一边).

returnType : a -> Type

我们如何实际使用此功能？据推测,它可以进入类型签名,因为它返回了一个类型.

 x : returnType 5

现在,这是一种完全不同于榆树中其他一切的类型签名.有一个数字文字(和一个函数)!突然间你可以开始写这样的东西了.

y = 5

x : returnType y
x = 6

这远远超出了Elm的类型系统所能做的.那种(令人兴奋的和强大的)类型级别和价值级别混合被称为依赖类型,并且不存在主流完全依赖类型的语言; 最接近主流的东西可能是Coq,Agda,Idris和ATS,它们都相当模糊.

至于字面上陈述的具有returnType : a -> String打印出表示值类型的字符串的函数的问题,这在Elm中也是不可能的,尽管出于其他原因.这样的函数(应用程序在运行时发生的事情)必须能够重建有关运行时值的类型信息,但Elm的运行时值只是Javascript值; 他们被剥夺了他们的榆树类型.您必须从Javascript值重建原始的Elm类型(并不总是可能,因为不同类型可能最终为相同的Javascript值)或者具有特殊的编译器支持.

在Elm REPL的情况下,选择后者.整个REPL是用Haskell编写的,并且充分利用了如何在Haskell运行时中实现Elm类型.