Gruppen 2 und 4
Samuel Teuber
propa@teuber.dev
https://teuber.dev/propa
fun1 xs = (xs == [])
fun2 f a = foldr f "a"
fun3 f a xs c = foldl f a xs c
fun4 f xs = map f xs xs
fun5 a b c = (maximum [a..b], 3 * c)
fun6 x y = succ (toEnum (last [fromEnum x..fromEnum y]))
fun7 x = if show x /= [] then x else error
fun1 xs = (xs == [])
fun1 :: (Eq t) => [t] -> Bool
fun2 f a = foldr f "a"
fun2 :: (Foldable c) => (a -> [Char] -> [Char]) -> b -> c a -> [Char]
fun3 f a xs c = foldl f a xs c
fun3 :: (Foldable t) => ((d -> e) -> a -> d -> e) -> (d -> e) -> t a -> d -> e
fun4 f xs = map f xs xs
Nicht typisierbar: Liste kann nicht auf xs angewendet werden
fun5 a b c = (maximum [a..b], 3 * c)
fun5 :: (Enum s, Ord s, Num t) => s -> s -> t -> (s, t)
-- What's Enum?
class Enum a where
toEnum :: Int -> a
fromEnum :: a -> Int
-- ...
succ :: a -> a
fun6 x y = succ (toEnum (last [fromEnum x..fromEnum y]))
fun6 :: (Enum a, Enum b, Enum c) => a -> b -> c
fun7 x = if show x /= [] then x else error
fun7 :: (Show ([Char] -> a)) => ([Char] -> a) -> ([Char] -> a)
-- weil:
error :: [Char] -> a
Beispiel für eine Datenstruktur
data Exp t
= Var t
| Const Integer
| Add (Exp t) (Exp t)
Beispiel für eine eval
Funktion:
eval :: Env a -> Exp a -> Integer
eval env (Var v) = env v
eval env (Const c) = c
eval env (Add e1 e2) = (eval env e1) + (eval env e2)
data Exp t
= Var t
| Const Integer
| Add (Exp t) (Exp t)
| Less (Exp t) (Exp t)
| And (Exp t) (Exp t)
| Not (Exp t)
| If (Exp t) (Exp t) (Exp t)
deriving Eq
eval :: Env a -> Exp a -> Integer
eval env (Var v) = env v
eval env (Const c) = c
eval env (Add e1 e2) = (eval env e1) + (eval env e2)
eval env (Less e1 e2)
| eval env e1 < eval env e2 = 1
| otherwise = 0
eval env (And e1 e2)
| eval env e1 == 0 || eval env e2 == 0 = 0
| otherwise = 1
eval env (Not e1)
| eval env e1 == 0 = 1
| otherwise = 0
eval env (If b t e)
| eval env b == 0 = eval env e
| otherwise = eval env t
instance Show a => Show (Exp a) where
show (Var a) = show a
show (Const i) = show i
show (Add e1 e2) = "(" ++ show e1 ++ " + " ++ show e2 ++ ")"
show (Less e1 e2) = "(" ++ show e1 ++ " < " ++ show e2 ++ ")"
show (And e1 e2) = "(" ++ show e1 ++ " & " ++ show e2 ++ ")"
show (Not e) = "!(" ++ show e ++ ")"
show (If b t e) = "(" ++ show b ++ " ? " ++ show t ++ " : " ++ show e ++ ")"
data Rope
= Leaf String
| Inner Rope Int Rope
ropeLength :: Rope -> Int
ropeLength (Leaf s) = length s
ropeLength (Inner _ w r) = w + ropeLength r
data Rope
= Leaf String
| Inner Rope Int Rope
ropeConcat :: Rope -> Rope -> Rope
ropeConcat l r = Inner l (ropeLength l) r
data Rope
= Leaf String
| Inner Rope Int Rope
ropeSplitAt :: Int -> Rope -> (Rope, Rope)
ropeSplitAt i (Leaf s) = (Leaf (take i s), Leaf (drop i s))
ropeSplitAt i (Inner l w r)
| i < w = let (ll, lr) = ropeSplitAt i l
in (ll, ropeConcat lr r)
| i > w = let (rl, rr) = ropeSplitAt (i-w) r
in (ropeConcat l rl, rr)
| otherwise = (l, r)
data Rope
= Leaf String
| Inner Rope Int Rope
ropeInsert :: Int -> Rope -> Rope -> Rope
ropeInsert i s rope = l `ropeConcat` s `ropeConcat` r
where (l, r) = ropeSplitAt i rope
data Rope
= Leaf String
| Inner Rope Int Rope
ropeDelete i j r = ropeConcat a d
where
(a, _) = ropeSplitAt i r
(_, d) = ropeSplitAt j r
$\lambda$-Terme
Bezeichnung | Notation | Beispiele aus der Vorlesung |
---|---|---|
Variablen | $x$ | $x$ $y$ $z$ |
Abstraktion | $\lambda x. t$ | $\lambda f.\lambda x. f x$ |
Funktionsanwendung | $t_1 t_2$ | $f y$ |
Wo würden hier die Klammern sitzen?
Umfrage
$t_1$ und $t_2$ heißen $α$-äquivalent, wennt $t_1$ in $t_2$ durch konsistente Umbenennung der λ-gebundenen Variablen überführt werden kann.
Beispiel: $$ \lambda x.(\lambda z.f(\lambda y.z\ y)\ x)=^\alpha\lambda y.(\lambda x.f(\lambda z.x\ z)\ y) $$
Extensionalitäts-Prinzip: 2 Funktionen gleich, wenn Ergebnis für alle Argumente gleich
Terme $λx.f\ x$ und $f$ heißen $\eta$-aquivalent, falls $x$ nicht freie Variable von f Beispiel:
- $\eta$-äquivalent: $f\ z$ und $\lambda x. f\ z\ x$
- nicht $\eta$-äquivalent: $g\ x$ und $\lambda x. g\ x\ x$
Umfrage
Der untypisierte $\lambda$-Kalkül ist konfluent:
Wenn $t \Rightarrow^* t_1$ und $t \Rightarrow^* t_2$,
dann gibt es ein $t'$ mit $t_1 \Rightarrow^* t'$ und $t_2 \Rightarrow^* t'$
Die Normalform eines $\lambda$-Terms $t$ ist - sofern sie existiert - eindeutig.
einfach weil es halt geht...
fib' n = fibAcc n 1 0
where fibAcc m acc1 acc0
| m == 0 = acc0
| m == 1 = acc1
| otherwise = fibAcc (m-1) (acc1+acc0) acc1
fib' 30
...endlich...
Eq
:class Eq t where
(==) :: t -> t -> Bool
(/=) :: t -> t -> Bool
x /= y = not (x == y)
x == y = not (x /= y)
instance Eq Bool where
True == True = True
False == False = True
x == y = False
Auch für Polymorphe Typen:
data Maybe t = Nothing | Just t
class Defaultable t where
getDefault :: t a -> a -> a
instance Defaultable Maybe where
getDefault (Just x) c = x
getDefault Nothing c = c
getDefault Nothing 1
getDefault (Just 10) 1
Typklasse für Datenstrukturen die Mappable
sind.
Wir wollen:
dMap
auf algebraischen Datentypen mit einem Parameter erlaubt class Mappable -- ...
Tree
instance Mappable Tree -- ...
-- Übungsaufgabe 5
class Mappable t where
dMap :: (a->b) -> t a -> t b
instance Mappable Tree where
dMap f t = treeMap f t