Understanding type family

6
votes

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.

1
haskelltype-families
Would it be clearer if it was written type family Times :: Nat -> Nat -> Nat where (...)? – AJF

1 Answers

10
votes

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