Haskell介绍

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

特点

最简单的语言 λ

语法:

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

最简单的语言 λ

规则:

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

    λx.axb == λy.ayb

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

    (λx.axb) y == ayb

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

    λx .f x == f

λ in Haskell

声明式语法

数据抽象

参数化类型

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

Currying

Eval strategy

Call by value

Call by name

Graph reduction (lazy eval)

Graph reduction (lazy eval)

Infinit data structure

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

Purity

Welcome to the real world

IO

IO

IO Monad

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 λ

定义:

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

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

规则:

  1. 函数类型:当 e1::a 且 e2::b,那么 (λe1.e2)::a->b
  2. 调用规则:当 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

Typeclass - Ad-hoc poly

Parametric polymorphism

Type inference

Type inference