Haskell

理解

思想不一定要用Haskell实现

名字源于Haskell Currying，柯里化的提出者

[!note] Curry-Howard同构:
这个同构关系是连接范畴论和类型论的关键桥梁。

之前的问题是不清晰的类型和需要维护的值
函数式编程，无状态（改变参数值），与数学物理一致

eg. find closest point

closestPoint :: Point -> [Point] -> Point 
closestPoint target = minimumBy (compare `on` distance target)

function

add :: Num a => a -> a -> a -- 类型签名，可以省略
add x y = x + y
x = add 1 1 -- 1 `add` 1

curry

foo = add 1 -- Num a=> a -> a

顺序

f a b c -- 这个函数等同于 (((f a) b) c)
($) :: (a -> b) -> a -> b
(.) :: (b -> c) -> (a -> b) -> a -> c
length (takeWhile (<1000) (scanl1 (+) (map sqrt [1..]))) + 1 -- 等价于 
(+1) $ length $ takeWhile (<1000) $ scanl1 (+) $ map sqrt [1..]

条件判断

safedive :: a -> a -> Maybe a
safedive x y = if notzero y then Maybe (x / y) else Nothing
	where Maybe a = Nothing | Just a --真实任意（反c）谓词
safediv x y --pipe
	| y /= 0 = Just (div x y) 
	| otherwise = Nothing

recursion

factorial :: Integer -> Integer
factorial 0 = 1
factorial n = n * factorial (n - 1)

[!Note] recursion vs iteration
recursion递归: 函数的定义用到了自身, 将复杂的问题简化, 最终到初始情况, 等价于数学归纳法. 实际计算浪费空间.
iteration迭代: 重复操作, 每次操作的输出是下次操作的输入, 逼近或求得所需目标. 引入额外的状态
二者等价,前者多用于数学(Haskell), 后者多用于计算机

linked lists

foo = [1, 2, 3]
-- foo = 1 : (2 : (3 : [])) same as math

sum :: Num a => [a] -> a
sum [] = 0
sum (x:xs) = x + sum xs

take :: Integer -> [a] ->[a]
take 0 _ = []
take - [] = []
take n (x:sx) = x : take (n - 1) xs

squareAll :: Num a => [a] -> [a]
squareAll xs = [x * x | x <- xs] --List Comprehension

Range
lazy evaluation

[1..20]
[1,3..9]
naturals = [0..]
-- naturals = naturalFrom 0
-- naturalsFrom x = x : naturalsFrom (x + 1)

Tuple (1,1.0,"ab")

higher order functions

lambda notation (anonymous function)

foo :: (a -> b) -> c
bar = foo (\x y -> x + y)

[!note] λ-calculus

λ-calculus

map

map :: (a -> b) -> [a] -> [b]

模块

import Data.List (nub，sort)
import Data.List hiding (nub)
import qualified Data.Map as M

类型类

class Eq a where
  (==), (/=) :: a -> a -> Bool
  x == y = not (x /= y)
  x /= y = not (x == y)

instance Eq Int where -- 实例
	x == y = intEq x y -- 假设 intEq 是比较两个 Int 的函数 
	x /= y = not (x == y)

有方法（态射）
可以提供默认实现
但不能保证满足约束，lean可以保证这点

类

构造
有属性，也可以有方法

data Shape = Circle Float| Rectangle Float Float --shape：类型类
Circle :: Float -> Shape --Circle：构造器
Circle 1.0 --实例化
module Shapes(..) --".."导出所有构造子

Record Syntax

data Car = Car {company :: String, model :: String, year :: Int}
Car {company="Ford", model="Mustang", year=1967}

导出类

data Shape = Circle Float| Rectangle Float Float deriving (Show) --deriving (Show)：导出Show类
data Bool = False | True deriving (Ord)
True > False --True
data Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday                
	deriving (Eq, Ord, Show, Read, Bounded, Enum)

别名

type String = [Char]

Functor & Monoid & Monad

范畴间的态射（同构）

id <$> == id
(f . g) <$> == f <$> . g <$>

这里指的是f可以自然诱导出函子

class Functor f where
        fmap :: (a -> b) -> f a -> f b
		(<$>) = fmap
        -- 构造器f天然是范畴中对象间的态射，fmap是范畴中态射的态射
        -- <$> is unique, f is confirmed by a & f a
instance Functor Maybe where
        fmap f Nothing = Nothing
        fmap f (Just a) = Just (f a)

这里的Applicative实际上是幺半群（monoid）

f <$> == pure f <*> -- 蕴含pure id <*> == id
pure (.) <*> u <*> v <*> w == u <*> (v <*> w)
pure f <*> pure x == pure (f x)

class (Functor f) => Applicative f where  
    pure :: a -> f a  -- 这里的a可以是函数等，注入、提升
    (<*>) :: f (a -> b) -> f a -> f b  
instance Applicative Maybe where 
	pure = Just 
	Nothing <*> _ = Nothing 
	(Just f) <*> = f <$>
Just (+3) <*> Just 9 -- Just 12

Monad单子:不可拆分, 组成其他对象
半:存在Monad没有把值拿出来的操作

Monad 是一个自函子范畴上的幺半群(对象)

(return x) >>= f == f x
m >>= return == m
(m >>= f) >>= g == m >>= (\x -> f x >>= g)

class Monad m where 
	return :: a -> m a -- 与pure对应
	(>>=) :: m a -> (a -> m b) -> m b 
	(>>) :: m a -> m b -> m b 
	x >> y = x >>= \_ -> y
instance Monad Maybe where 
	return x = Just x 
	Nothing >>= f = Nothing 
	Just x >>= f = f x

语法糖do

safeDiv a b >>= (\x ->
safeDiv c x >>= (\y ->
safeDiv d y >>= (\z ->
  safeDiv e z)))

val = do
  x <- safeDiv a b
  y <- safeDiv c x
  z <- safeDiv d y
  safeDiv e z

内部状态, 如Maybe

Just 4 >>= tentime --Just 40

外部状态, IO隔绝副作用, 不可能消除

IO :: world -> world -> () --()Unit

运算符

• 单参数函数：<$>（或 fmap）。
• 多参数函数：liftA2 或链式 <$> 和 <*>。
• 顺序执行且需传递结果：>>=（Monad）。
• 顺序执行但忽略结果：*> 或 >>。
• 错误处理/回退：<|>（Alternative）。
• 组合 Monadic 函数：>=> 或 <=<。

尾递归优化

重用当前栈帧

def factorialTailRec (n : Nat) : Nat :=
  let rec aux (n : Nat) (acc : Nat) : Nat :=
    match n with
    | 0 => acc
    | n + 1 => aux n (acc * (n + 1))
  aux n 1

环境

ghci：命令行界面
:+命令
? help
t type
l load
r reload
i info
e edit
q quit
多行;隔开或:{ :}

.hs

Hoogle查找函数

例子（函数外延性）：
传统类型论中，需要假设：

coq

Axiom fun_ext : ∀ (f g : A → B), (∀ x, f x = g x) → f = g.

而在 HoTT 中，这是 Univalence 的推论，无需额外公理。