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