理解`5 1'的类型

Question

我在这里使用了这个Haskell解释器:https://tryhaskell.org/

当我提供输入时,5 1它告诉我 - 我假设它是类型 - 表达式是类型(Num a, Num (a -> t)) => t:

? 5 1
:: (Num a, Num (a -> t)) => t

现在我试着理解如何解释这个,这就是我提出的.

a是任何Num类型,所以是a -> t.表达式导致某种类型t通过理论上应用1(类型a)到5(类型a -> t)而产生.

这真的让我感到不安,因为我看不出约束是否Num (a -> t)有意义.从理论上讲,它看起来是正确的解释,但我无法找到证明.

---

解释是正确的

这是有道理的,因为它Num是一个多态类型 - 可以是一个函数.

Answer 1

数字在Haskell中是多态的.当你写的东西像

5

编译器将其转换为fromInteger (5 :: Integer) :: Num a => a.编译器事先不知道要使用什么实例,所以它最好从上下文中猜测.如果你有5 1,那么第一个数字是多态Num类型,也必须是一个函数.第二个数字只是一个Num,所以这是很正常的.

但你可能会问"一个数字怎么能成为一个函数？" 如果世界上的一切都有意义,那么数字就不是函数,但你实际上可以为它们编写一个实例,或多或少:

{-# LANGUAGE FlexibleInstances #-}

instance Num a => Num (a -> a) where
    fromInteger a = const (fromInteger a)
    a + b = \c -> a c + b c
    a * b = \c -> a c * b c
    abs a = \c -> abs (a c)
    signum a = \c -> signum (a c)
    negate a = \c -> negate (a c)

这满足了定义,但它可能不会非常有用.例如:

> let x = 1 :: Int -> Int; y = 2 :: Int -> Int
> x + y $ 0
3
> x + y $ 102089
3
> x + y $ undefined
3

所以在这里,论证与表达无关,甚至没有评估.一个更有趣的一个:

> let x = (+10); y = (*10)
> x + y $ 0    -- x 0 + y 0 = 0 + 10 + 0 * 10
10
> x + y $ 1    -- x 1 + y 1 = 1 + 10 + 1 * 10
21
> x + y $ 2
32

等等.我相信有人可以找到一个有趣的用例,但我不推荐它,它显然不是很直观.