Haskell介绍

Authors:	黄毅 <yi.codeplayer@gmail.com>
Date:	2011年 03月 25日

特点

Functinal
Pure
Lazy
Type system
Type inference

最简单的语言 λ

语法：

表达式 ::= 标识符

表达式 ::= λ标识符.表达式

最简单的语言 λ

规则：

α-变换 (形参命名) ::

λx.axb == λy.ayb

β-归约 (函数调用) ::

(λx.axb) y == ayb

η-变换 (函数化简 Pointfree Style) ::

λx .f x == f

λ in Haskell

```
\x -> x + x
```
```
add = \x y -> x + y
```
```
:ghci> add 1 2
3
```

声明式语法

```
add x y = x + y
```

elem x [] = False
elem x (y:ys) = x==y ||
                (elem x ys)

数据抽象

data Customer = Customer {
      customerID      :: Int
    , customerName    :: String
    , customerAddress :: String
    }

:t Customer
Customer :: Int -> String ->
              String -> Customer
:t customerID
customerID :: Customer -> Int

参数化类型

data Maybe a = Just a
             | Nothing

:ghci> :t Nothing
Nothing :: Maybe a
:ghci> :t Just
Just :: a -> Maybe a

Pattern match and Guard

find :: Int -> [Customer] ->
             Maybe Customer
find _ [] = Nothing
find id (x@(Customer cid _ _):xs)
    | cid==id = Just x
    | otherwise = find id xs

Prefix or Infix

```
add x y = x + y
```
```
add x y = (+) x y
```
```
add = (+)
```

x `elem` [] = False
x `elem` (y:ys) = x==y ||
         (x `elem` ys)

Currying

```
:ghci> add 1 2
3
```
```
:ghci> (add 1) 2
3
```

:ghci> :t add 1
add 1 :: Integer -> Integer

Eval strategy

call by value
call by name
call by need

Call by value

(λx.x*x) (λx.x+x 1)
(λx.x*x) (1+1)
(λx.x*x) 2
2*2
4

Call by name

(λx.x*x) (λx.x+x 1)
(λx.x+x 1)*(λx.x+x 1)
(1+1)*(1+1)
2*2
4

Graph reduction (lazy eval)

(λx.x*x) (λx.x+x 1)

Graph reduction (lazy eval)

(λx.x+x 1)*(λx.x+x 1)

Infinit data structure

:ghci> take 5 $
        filter even
            [1,2..]
[2,4,6,8,10]

Purity

Immutable data
No side effects
Referential transparency

Welcome to the real world

#!/usr/bin/python
while True:
    print '>>',
    name = raw_input()
    print 'Welcome', name

```
>> huangyi
Welcome huangyi
>>
```

IO

raw_input :: RealWorld ->
             (String, RealWorld)
print :: String ->
         RealWorld ->
         RealWorld

伪码：

(_, w2) = (print ">>") w1
(name, w3) = raw_input w2
(_, w4) = (print "Welcome "++name) w3

IO

type IO a = RealWorld ->
            (a, RealWorld)

raw_input :: IO String
print :: String -> IO ()

>>= :: IO a ->
       (a -> IO b) ->
       IO b

IO Monad

(print ">>") >>= \_ ->
raw_input >>= \name ->
print ">>"++name

do
  print ">>"
  name <- raw_input
  print "Welcome "++name

IO Monad

class Monad m where
    >>= :: m a ->
           (a -> m b) ->
           m b
    >> :: m a -> m b -> m b
    ma >> mb = ma >>= \_->mb

    return :: a -> m a

Type system

第三次数学危机
Simply Typed λ
Curry–Howard correspondence
Polymorphism
Dependent type

作用

程序正确性证明
阻止坏程序
允许好程序

坏程序

整数和字符串相加
长度和重量相加
整数加法溢出
数组访问越界
排序算法返回结果无序

Simply Typed λ

定义：

如果a和b是类型，那么(a->b)也是类型。

e::a 表示表达式e的类型是a。

规则：

函数类型：当 e1::a 且 e2::b，那么 (λe1.e2)::a->b

调用规则：当 e1::a->b 且 e2::a，那么 (e1 e2)::b

Curry–Howard correspondence

(A ∧ B) ≡ (A, B)

(A ∨ B) ≡ Either A B

A ⇒ B ≡ A -> B

¬A ≡ A->undefined

Curry–Howard correspondence

A ⇒ A ∨ B
Left :: A -> Either A B

A ∧ B ⇒ A
fst :: (A, B) -> A

(A ⇒ (B ⇒ C)) ⇒ ((A ∧ B) ⇒ C)
proof :: (A -> (B -> C)) -> (A, B) -> C
proof f (a, b) = (f a) b

Polymorphism

Subtyping polymorphism (class继承)
Ad-hoc polymorphism (函数重载)
Parametric polymorphism (泛型)

Typeclass - Ad-hoc poly

class Eq a where
    (==) :: a -> a -> Bool

```
instance Eq Int where
    (==) = eqInt
```

instance (Eq a, Eq b) =>
         Eq (a, b) where
    (a1, b1)==(a2, b2) =
        (a1==a2 && b1==b2)

:ghci> :t (==)
(==) :: Eq a => a -> a -> Bool

Parametric polymorphism

```
head (x:xs) = x
```

map :: (a->b) -> [a] -> [b]
map _ [] = []
map f (x:xs) = (f x):(map f xs)

Type inference

```
:ghci> :t (\x -> x)
```
```
(\x -> x) :: t -> t
```
```
:ghci> :t (\x -> x+x)
```
```
(\x -> x+x) :: Num a => a -> a
```
```
:ghci> :t 1
```
```
1 :: Num a => a
```
```
:ghci> :t head
```
```
head :: [a] -> a
```

Type inference

```
:ghci> :t \x -> (head x) + 1
```

\x -> (head x) + 1 :: Num a => [a] -> a

```
:ghci> :t map
```
```
map :: (a -> b) -> [a] -> [b]
```
```
:ghci> :t (+ 1)
```
```
(+ 1) :: Num a => a -> a
```
```
:ghci> :t map (+1)
```
```
map (+1) :: Num b => [b] -> [b]
```