Error and correct code

Question

I relied heavily on a system like haskell to avoid errors and looked for whether it could be used to provide a (weak?) Form of code correctness.

The code correctness form that I have in mind is as follows:

The function is f :: a -> btrue if it is fguaranteed to return a type output bfor any type input a. This clearly fails for the well-known head ( head:: [a] -> a) function .

In one way, I know that the type system cannot guarantee this form of validity when the code uses error ( error :: Char -> a). The error function pretty much redefines the entire type system, so I would like to avoid using this function unless explicitly provided for.

My question is double:

• What other functions (or haskell fragments) are exceptions for the Haskell type system except errors?

• More importantly, is there a way to prevent the use of such functions in the Haskell module?

Many thanks!

Answer 1

You can write your own functions that never give meaning. Consider the following function:

never :: a -> b
never a = never a

It does not end, therefore it is considered a value _|_(pronounced bottom ). All types in Haskell are actually the sum of the type and this special value .

You can also write a function that is only partially defined, for example

undefinedForFalse :: Bool -> Bool
undefinedForFalse True = True

undefinedForFalse False - undefined, , _|_, , , , .

error , _|_, , , , , .

Haskell , _|_, , _|_. , _|_, "total". , , _|_ , " ". , , " " " ". , .

Answer 2

, . , . Cirdec, , ( ) .

- : , ( error, undefined ).

(a -> b) -> a -> b. .

, f A B r :: [a] -> [a] , r . map f = map f . r. " " map. .

A ( ) , , mapper :: (a -> b) -> F a -> F b mapper id = id, , mapper f . mapper g = mapper (f . g). , fmap f, Functor. "" .

: ! http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf