Understanding type family

Question

I have the following code:

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

I know that type families allow you to write functions on the type level. However, for the code above, I know that (a :: Nat) (b :: Nat) are the types of the two parameters that are passed to the function Times.

However I don't understand what the final :: Nat after (a :: Nat) (b :: Nat) means. Any insights are appreciated.

Answer 1

The final :: Nat indicates that the type-level function returns a Nat.