Haskell Recursive Factorial Implementation

factorial.hs

-- Compute the factorial of n recrusively

module Factorial where

factorial :: Int -> Int
factorial 0 = 1
factorial n = n * factorial (n-1)

Funny enough I'm now at a point where I understand what a basic type class is so that I can understand what you mean.
For dependent typing in Haskell it seems you have to turn on a flag (personally I want to get solid on the basis before I start using flags).<

I wonder however if this could be done with just the normal non dependent type classes that Haskell offers.
And I assume you are using the pattern matching instead of the product because if so you would have to define how Nonnegative and Positive behave for lists right ?

And I assume you are using the pattern matching instead of the product because if so you would have to define how Nonnegative and Positive behave for lists right ?

The reason I didn't use product is because multiplication of two Nonnegative integers is not guaranteed to be Positive - that is, 0 multiplied by any Nonnegative will be 0 (not Positive). Therefore, we can't implement a function (*) :: Nonnegative -> Nonnegative -> Positive and have it return a correct result (so product won't work here since it uses (*) in its implementation).

In the version with pattern matching, we use the 0 case as the base case. If we have a proof that 0 is the only Nonnegative number that is not Positive (which might even be by definition), then the pattern matching on n will be guaranteed to be a multiplication of two Positive integers (which will always give us a Positive). Unfortunately, I think we need dependent typing for such a clean solution.

If you want to convert a Nonnegative to a Positive in Haskell (without a flag), you'll need to handle the case where 0 is passed as input (which you can do with Maybe). A function definition might look toPositive :: Nonnegative -> Maybe Positive. So yes, it's definitely possible.

Just to be clear, this doesn't have anything to do with how the types behave for lists. Since a list is a monad, it can "wrap" any type.