Reputation: 2011
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
Reputation: 152682
The final :: Nat
indicates that the type-level function returns a Nat
.
Upvotes: 10