Formal Methods
DR QAMAR UZ ZAMAN
Types
Definition : Type is a name for a collection of related values.
Syntax :
: type
:t
Built-in types :
o Bool = True & False o Int = Numbers
o String = List of characters o Char = Single character
o Float = Decimal numbers
Errors
Common errors are produced because of types.
Types Error :
o Apply function to one or more arguments to a wrong type
Example :
prelaude > 1 + False
(type error)
Expressions Types
Expression evaluate type (resultant will also have a type )
e :: type
Expression
Example 1 : Example 2 :
> not False > 2+2
> True >4
> : type not False > : type 2+2
>not False :: Bool > 2+2 :: Int
List Types
o A sequence of values of same type.
not a set (values can duplicate )
Example :
[ False , True , False ] : : [ Bool ]
[ ‘a’ , ‘b’ , ‘c’ ] : : [ Char ]
o [ t ] is the type of list with elements of type t.
Example :
[ [ ‘a’ ] , [ ‘b’ , ‘c’ ] ] : : [ [ Char ] ]
Tuple
Tuple is a sequence of values of different types.
o It is not necessary that they should be different types.
o No restriction on number of elements.
Example :
( False , True ) : : ( Bool , Bool )
same type
( False , ‘a’ , 1 ) : : ( Bool , Char , Int )
different type
Tuple (Cont. )
( t1 , t2 , . . tn ) : : ( Types )
o Type of tuple can tell the length .
o Tuple of Tuple can exist
Example :
(‘a’ , (False , ‘b’) ) : : ( Char , ( Bool , Char ) )
( True , [ True , False ] ) : : ( Bool , [ Bool ] )
[ (‘a’ , ‘b’) , (‘c’ , ‘d’ ) ] : : [ ( Char ) , ( Char ) ]
List of tuple
Function Types
o Mapping from value of one type to value of another type.
Example :
not : : Bool Bool
even : : Int Bool
o In General
t1 t 2
Type of Type of
Argument Result
Function Types (Cont.)
o Arguments and result are unrestricted
Function can have multiple Arguments.
Function can return multiple tuples
Function can also return a function
Example 1 : Example 2 :
add : : ( Int , Int ) Int zeroton : : Int [ Int ]
type type
add ( x , y ) = x + y zeroton n = [ 0..n ]
definition definition
Curried Function
Function with multiple arguments are possible by returning function as result
Example :
add’ : : Int Int Int
add’ x y = x + y
Returns
add x
Returns
x+y
> add 3 2
Curried Function (Cont.)
mult : : Int Int Int Int
mult x y z = x * y * z OR mult ( x , y , z ) = x * y * z
Curried function are more flexible then functions on tuples.
Because : Functions can often can be made by partially applying.
(Tuples take all parameters to complete / run )
Polymorphic Functions
A function that can evaluate to or be applied to values of different types
o Otherwise you have to create different functions for different types
Example : Length function
o Returns length regardless if it is String / Char / Int / Float / Bool
o Type :
length : : [ a ] Int
generic type variable
o a , b , c .. etc can be used in Haskell as generic variables
Overloaded Function
o Constraints on number of arguments in a function
o If we apply constraints on polymorphic function then it becomes overloaded
function
Example :
( + ) : : Num a => a --> a --> a
Constraint
o Only works on numeric value
o Doesnot work on String or Char
Constraints
Example : Type error :
o Num >1+2 > ‘a’ + ‘b’
( + ) : : Num a => a --> a --> a >3
o Order >8>9 > 8 > ‘h’
( > ) : : Ord a => a --> a --> Bool > False
o Equality > 6 == 6 > 0 == ‘r’
( == ) : : Eq a => a --> a --> Bool > True
Function Conditions
Two types of Conditions :
1. If ( cannot exist without else)
Example 1 :
abs : : Int Int
abs n = if n > 0 then n else –n
Example 2 :
signnum : : Int Int
signnum n = if n > 0 then 1 else
if n < 0 then -1 else 0
Function Condition (Cont.)
2. Guard ( | )
o Easy and no issue of spaces
Example 1 :
abs n | n > 0 = n
| n < 0 = -n OR | otherwise = -n
Example 2 :
signnum n | n > 0 = 1
| n < 0 = -1
| n == 0 = 0
Pattern Matches
Simplifying our codes by identifying specific types of expression
Example : All strings start with ‘a’
Example
&& : : Bool Bool Bool && True True = True && True True = True
&& True True = True && _ _ = False && True b = b
&& True False = False
&& False True = False Whatever other
&& False False = False
List Patterns
o (x:xs) is a pattern that matches a non-empty list which is formed by something
o:[]
Example :
[1 , 2 , 3 , 4 ]
1:(2:(3:(4:[])))
head : : [a] a
head (x : xs) = x
head ( x : _ ) = x (more efficient because Haskell is lazy)
tail ( _ : xs ) = xs
