伊德里斯的胖箭

Question

我希望这个问题适合这个网站,它只是选择Idris中与Haskell相比的具体语法,因为两者非常相似.我想这并不重要,但我对此非常好奇.Idris =>用于Haskell使用的某些情况->.到目前为止,我已经看到Idris仅用于->函数类型以及=>lambda和case _ of.这种选择是否来自于认识到在这些用例之间有明确的语法区别在实践中是否有用？这只是一种随意的化妆品选择而我是在过度思考吗？

Answer 1

好吧,在Haskell中,类型签名和值在不同的命名空间中,因此在一个中定义的东西不会与另一个中的某些东西发生冲突.在Idris中,类型和值占用相同的命名空间,这就是为什么你没有data Foo = Foo像在Haskell中看到的那样,而是,data Foo = MkFoo- 调用类型Foo,并调用构造函数MkFoo,因为已经存在一个值(类型)Foo),绑定到名称Foo,例如data Pair = MkPair http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#tuples 所以它可能是最好的,它没有尝试使用用于构建函数的类型,用于lambda的箭头 - 这些是相当不同的东西.你可以将它们与例如the (Int -> Int) (\x => x).