[Haskell-beginners] Further constraining types

[Christopher Howard]

On 08/05/2011 01:10 PM, Brent Yorgey wrote:
>
> Sorry, I meant this is how you would do it in Agda.  It is not
> possible to do this directly in Haskell (because Haskell does not have
> dependent types). (There are ways of "faking" some dependent types in
> Haskell with type-level-programming techniques... but they can be
> quite convoluted and would definitely be taking this email too far
> afield.)
>

{-
   Supposing for now we set aside dependent types, I'm thinking that the 
closest I get to my ideal is a combination of safe constructors and 
law-style rewriting. I'm thinking this could be workable:
-}

module Natural ( Natural(), natural, (==), (+), (-), (*),
                  abs, signum, fromInteger ) where

data Natural = Natural Integer | Indeterminate deriving (Show)

-- fundamental constructor

natural :: Integer -> Natural
natural n | n < 0 = Indeterminate
natural n = Natural n

-- trying to fit it into the Num class

instance Eq Natural where

-- very controversial, but necessary to satisfy signum law
   (==) Indeterminate Indeterminate = True
   (==) Indeterminate _             = False
   (==) _             Indeterminate = False
   (==) (Natural a)   (Natural b) | a == b    = True
                                  | otherwise = False

instance Num Natural where

   Indeterminate + _             = Indeterminate
   _             + Indeterminate = Indeterminate
   (Natural a)   + (Natural b)   = Natural ((Prelude.+) a b)

   Indeterminate - _             = Indeterminate
   _             - Indeterminate = Indeterminate
   (Natural a)   - (Natural b) | a < b     = Indeterminate
                               | otherwise = Natural ((Prelude.-) a b)

   Indeterminate * _             = Indeterminate
   _             * Indeterminate = Indeterminate
   (Natural a)   * (Natural b) | a < 0 || b < 0 = Indeterminate
                               | otherwise      = Natural ((Prelude.*) a b)

   abs Indeterminate = Indeterminate
   abs (Natural a)   = (Natural a)

   signum Indeterminate = Indeterminate
   signum (Natural 0) = (Natural 0)
   signum (Natural a) = (Natural 1)

   fromInteger n = natural n

{-
   Fundamentally, this is not really much different than using a 
constructor that returns a Maybe value. But it does gives me a much more 
"natural" type syntax, while still allowing my calculations to error-out 
without bottoms or crashes.

   Thoughts?
-}

-- 
frigidcode.com
theologia.indicium.us