了解类型家庭

Question

我有以下代码：

{-# LANGUAGE TypeFamilies #-}
type family Times (a :: Nat) (b :: Nat) :: Nat where 
   Times Z n = Z
   Times (S m) n = Plus n (Times m n)

我知道类型家族允许您在类型级别上编写函数。但是，对于上面的代码，我知道(a :: Nat) (b :: Nat)这是传递给函数的两个参数的类型Times。

但是我不明白决赛:: Nat之后(a :: Nat) (b :: Nat)意味着什么。任何见解都表示赞赏。

Answer 1

最终:: Nat指示类型级别的函数返回a Nat。