函数返回类型未强制执行

Question

如果有耐心的人向我解释下面的情况,我将非常感激.在我看来,好像Haskell准备好在从函数返回值时执行某种整数类型的强制.另一方面,我已经读过Haskell永远不会隐式转换类型.

如果我输入GHCi:

> import Data.Word
> let t :: (Integer, Word32); 
      t = let { y = fromIntegral (-1)     -- line breaks added for readability
              ; y' :: Integer 
              ; y' = fromIntegral y } in (y', y)

GHCi后来告诉我t = (-1,4294967295).但是,如果我将本地y类型专门限制为Word32:

> let t :: (Integer, Word32); 
      t = let { y :: Word32
              ; y = fromIntegral (-1)     -- line breaks added for readability
              ; y' :: Integer
              ; y' = fromIntegral y } in (y', y)

GHCi会告诉我的t = (4294967295,4294967295).

我认为,如果t"S型陈述explicite为(Integer, Word32),GHCI会得出这样的结论y' :: Integer,并y :: Word32自该函数的结果是(y', y).然后,类型定义y :: Word32将是完全不必要的.

这一切都始于我试图编写一个函数来"安全地"转换Integral类成员 - 例如Int - > Word32.该函数意味着Just 1在传递1和Nothing传递时返回-1.

通过搜索引擎优化和互联网进行的简短搜索没有给我任何解释.

Answer 1

我认为,如果t"S型陈述explicite为(Integer, Word32),GHCI会得出这样的结论y' :: Integer,并y :: Word32自该函数的结果是(y', y).

不,这并不推断该类型的东西y'和y.它只是检查它们是否与预期的类型兼容.一个更简单的例子¹:

x = -1

y :: Integer
y = x

y' :: Word32
y' = x

哪种类型x有？它既不是Integer也不是Word32.这是文字的类型:

x :: Num a => a
x = fromInteger (-1 :: Integer)

并且Num a => a兼容作为Integerin y和as Word32in 的用法y'.无论如何x使用,其类型x仅取决于术语的定义方式.

要解释您的结果,请记住引用透明度 - 我们可以用它们的定义替换变量:

t = let y = fromIntegral (-1)
        y' = (fromIntegral y) :: Integer
    in (y', y) :: (Integer, Word32)

扩展到

t = ( (fromIntegral (fromIntegral (-1))) :: Integer -- nothing says Word32 here
    , fromIntegral (-1)
    ) :: (Integer, Word32)

而第二个

t = let y = (fromIntegral (-1)) :: Word32
        y' = (fromIntegral y) :: Integer
     in (y', y) :: (Integer, Word32)

扩展到

t = ( (fromIntegral ( (fromIntegral (-1)) :: Word32 )) :: Integer
    , (fromIntegral (-1)) :: Word32
    ) :: (Integer, Word32)

_{1:我希望可怕的单态限制不会在这里弄乱我们.任何更有知识的人都可以确认它不适用于x(或在什么情况下)？}