Authors: | 黄毅 <yi.codeplayer@gmail.com> |
---|---|
Date: | 2011年 03月 25日 |
语法:
- 表达式 ::= 标识符
- 表达式 ::= λ标识符.表达式
规则:
- α-变换 (形参命名) ::
λx.axb == λy.ayb
- β-归约 (函数调用) ::
(λx.axb) y == ayb
- η-变换 (函数化简 Pointfree Style) ::
λx .f x == f
\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
find :: Int -> [Customer] ->
Maybe Customer
find _ [] = Nothing
find id (x@(Customer cid _ _):xs)
| cid==id = Just x
| otherwise = find id xs
add x y = x + y
add x y = (+) x y
add = (+)
x `elem` [] = False
x `elem` (y:ys) = x==y ||
(x `elem` ys)
:ghci> add 1 2
3
:ghci> (add 1) 2
3
:ghci> :t add 1
add 1 :: Integer -> Integer
(λx.x*x) (λx.x+x 1)
(λx.x+x 1)*(λx.x+x 1)
:ghci> take 5 $
filter even
[1,2..]
[2,4,6,8,10]
#!/usr/bin/python
while True:
print '>>',
name = raw_input()
print 'Welcome', name
>> huangyi Welcome huangyi >>
raw_input :: RealWorld ->
(String, RealWorld)
print :: String ->
RealWorld ->
RealWorld
伪码:
(_, w2) = (print ">>") w1
(name, w3) = raw_input w2
(_, w4) = (print "Welcome "++name) w3
type IO a = RealWorld ->
(a, RealWorld)
raw_input :: IO String
print :: String -> IO ()
>>= :: IO a ->
(a -> IO b) ->
IO b
(print ">>") >>= \_ ->
raw_input >>= \name ->
print ">>"++name
do
print ">>"
name <- raw_input
print "Welcome "++name
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
定义:
如果a和b是类型,那么(a->b)也是类型。
e::a 表示表达式e的类型是a。
规则:
- 函数类型:当 e1::a 且 e2::b,那么 (λe1.e2)::a->b
- 调用规则:当 e1::a->b 且 e2::a,那么 (e1 e2)::b
(A ∧ B) ≡ (A, B)
(A ∨ B) ≡ Either A B
A ⇒ B ≡ A -> B
¬A ≡ A->undefined
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
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
head (x:xs) = x
map :: (a->b) -> [a] -> [b]
map _ [] = []
map f (x:xs) = (f x):(map f xs)
: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
: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]