ceno980
ceno980

Reputation: 2011

Understanding type family

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.

Upvotes: 6

Views: 112

Answers (1)

Daniel Wagner
Daniel Wagner

Reputation: 152682

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

Upvotes: 10

Related Questions