Skip to content

Commit e22342c

Browse files
committed
haskell hw0-3
1 parent b27c494 commit e22342c

37 files changed

+4521
-0
lines changed

haskell/hw0/app/Main.hs

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
module Main
2+
( main,
3+
)
4+
where
5+
6+
main :: IO ()
7+
main = putStrLn "There is no main"

haskell/hw0/hw-0.md

+149
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
Homework #0
2+
===========
3+
4+
[Classroom](https://classroom.github.com/a/SrRMYdgl)
5+
6+
Task 1
7+
------
8+
9+
1. Create a module named `HW0.T1` and define the following type in it:
10+
11+
```
12+
data a <-> b = Iso (a -> b) (b -> a)
13+
14+
flipIso :: (a <-> b) -> (b <-> a)
15+
flipIso (Iso f g) = Iso g f
16+
17+
runIso :: (a <-> b) -> (a -> b)
18+
runIso (Iso f _) = f
19+
```
20+
21+
2. Implement the following functions and isomorphisms:
22+
23+
```
24+
distrib :: Either a (b, c) -> (Either a b, Either a c)
25+
assocPair :: (a, (b, c)) <-> ((a, b), c)
26+
assocEither :: Either a (Either b c) <-> Either (Either a b) c
27+
```
28+
29+
Task 2
30+
------
31+
32+
1. Create a module named `HW0.T2` and define the following type in it:
33+
34+
```
35+
type Not a = a -> Void
36+
```
37+
38+
2. Implement the following functions and isomorphisms:
39+
40+
```
41+
doubleNeg :: a -> Not (Not a)
42+
reduceTripleNeg :: Not (Not (Not a)) -> Not a
43+
```
44+
45+
Task 3
46+
------
47+
48+
1. Create a module named `HW0.T3` and define the following combinators in it:
49+
50+
```
51+
s :: (a -> b -> c) -> (a -> b) -> (a -> c)
52+
s f g x = f x (g x)
53+
54+
k :: a -> b -> a
55+
k x y = x
56+
```
57+
58+
2. Using *only those combinators* and function application (i.e. no lambdas,
59+
pattern matching, and so on) define the following additional combinators:
60+
61+
```
62+
i :: a -> a
63+
compose :: (b -> c) -> (a -> b) -> (a -> c)
64+
contract :: (a -> a -> b) -> (a -> b)
65+
permute :: (a -> b -> c) -> (b -> a -> c)
66+
```
67+
68+
For example:
69+
70+
```
71+
i x = x -- No (parameters on the LHS disallowed)
72+
i = \x -> x -- No (lambdas disallowed)
73+
i = Prelude.id -- No (only use s and k)
74+
i = s k k -- OK
75+
i = (s k) k -- OK (parentheses for grouping allowed)
76+
```
77+
78+
Task 4
79+
------
80+
81+
1. Create a module named `HW0.T4`.
82+
83+
2. Using the `fix` combinator from the `Data.Function` module define the
84+
following functions:
85+
86+
```
87+
repeat' :: a -> [a] -- behaves like Data.List.repeat
88+
map' :: (a -> b) -> [a] -> [b] -- behaves like Data.List.map
89+
fib :: Natural -> Natural -- computes the n-th Fibonacci number
90+
fac :: Natural -> Natural -- computes the factorial
91+
```
92+
93+
Do not use explicit recursion. For example:
94+
95+
```
96+
repeat' = Data.List.repeat -- No (obviously)
97+
repeat' x = x : repeat' x -- No (explicit recursion disallowed)
98+
repeat' x = fix (x:) -- OK
99+
```
100+
101+
Task 5
102+
------
103+
104+
1. Create a module named `HW0.T5` and define the following type in it:
105+
106+
```
107+
type Nat a = (a -> a) -> a -> a
108+
```
109+
110+
2. Implement the following functions:
111+
112+
```
113+
nz :: Nat a
114+
ns :: Nat a -> Nat a
115+
116+
nplus, nmult :: Nat a -> Nat a -> Nat a
117+
118+
nFromNatural :: Natural -> Nat a
119+
nToNum :: Num a => Nat a -> a
120+
```
121+
122+
3. The following equations must hold:
123+
124+
```
125+
nToNum nz == 0
126+
nToNum (ns x) == 1 + nToNum x
127+
128+
nToNum (nplus a b) == nToNum a + nToNum b
129+
nToNum (nmult a b) == nToNum a * nToNum b
130+
```
131+
132+
Task 6
133+
------
134+
135+
1. Create a module named `HW0.T6` and define the following values in it:
136+
137+
```
138+
a = distrib (Left ("AB" ++ "CD" ++ "EF")) -- distrib from HW0.T1
139+
b = map isSpace "Hello, World"
140+
c = if 1 > 0 || error "X" then "Y" else "Z"
141+
```
142+
143+
2. Determine the WHNF (weak head normal form) of these values:
144+
145+
```
146+
a_whnf = ...
147+
b_whnf = ...
148+
c_whnf = ...
149+
```

haskell/hw0/hw0.cabal

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
cabal-version: 2.0
2+
name: hw0
3+
version: 0.1.0.0
4+
5+
author: letstatt
6+
build-type: Simple
7+
8+
executable hw0
9+
main-is: Main.hs
10+
build-depends: base ^>=4.14.3.0
11+
hs-source-dirs: app
12+
default-language: Haskell2010
13+
14+
library
15+
hs-source-dirs: src
16+
exposed-modules: HW0.T1, HW0.T2, HW0.T3, HW0.T4, HW0.T5, HW0.T6
17+
ghc-options: -Wall
18+
build-depends: base >= 4.9 && <5
19+
default-language: Haskell2010

haskell/hw0/src/HW0/T1.hs

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
{-# LANGUAGE TypeOperators #-}
2+
3+
module HW0.T1 (type (<->)(Iso), flipIso, runIso, distrib, assocPair, assocEither) where
4+
5+
data a <-> b = Iso (a -> b) (b -> a)
6+
7+
flipIso :: (a <-> b) -> (b <-> a)
8+
flipIso (Iso f g) = Iso g f
9+
10+
runIso :: (a <-> b) -> (a -> b)
11+
runIso (Iso f _) = f
12+
13+
distrib :: Either a (b, c) -> (Either a b, Either a c)
14+
distrib (Left a) = (Left a, Left a)
15+
distrib (Right (b, c)) = (Right b, Right c)
16+
17+
assocPair :: (a, (b, c)) <-> ((a, b), c)
18+
assocPair = Iso (\(a, (b, c)) -> ((a, b), c)) (\((a, b), c) -> (a, (b, c)))
19+
20+
assocEitherLeftMatcher :: Either a (Either b c) -> Either (Either a b) c
21+
assocEitherLeftMatcher (Left a) = Left (Left a)
22+
assocEitherLeftMatcher (Right (Left b)) = Left (Right b)
23+
assocEitherLeftMatcher (Right (Right c)) = Right c
24+
25+
assocEitherRightMatcher :: Either (Either a b) c -> Either a (Either b c)
26+
assocEitherRightMatcher (Left (Left a)) = Left a
27+
assocEitherRightMatcher (Left (Right b)) = Right (Left b)
28+
assocEitherRightMatcher (Right c) = Right (Right c)
29+
30+
assocEither :: Either a (Either b c) <-> Either (Either a b) c
31+
assocEither = Iso assocEitherLeftMatcher assocEitherRightMatcher

haskell/hw0/src/HW0/T2.hs

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
module HW0.T2 (Not, doubleNeg, reduceTripleNeg) where
2+
3+
import Data.Void (Void)
4+
5+
type Not a = a -> Void
6+
7+
-- doubleNeg :: a -> Not (Not a)
8+
-- a -> Not (a -> Void)
9+
-- a -> (a -> Void) -> Void
10+
doubleNeg :: a -> Not (Not a)
11+
doubleNeg a f = f a
12+
13+
-- reduceTripleNeg :: Not (Not (Not a)) -> Not a
14+
-- Not (Not (Not a)) -> Not a
15+
-- Not (Not (a -> Void)) -> (a -> Void)
16+
-- Not ((a -> Void) -> Void) -> (a -> Void)
17+
-- (((a -> Void) -> Void) -> Void) -> (a -> Void)
18+
-- (((a -> Void) -> Void) -> Void) -> a -> Void
19+
-- f a = (((a -> Void) -> Void) -> Void)
20+
-- f a = ((a -> Void) -> Void) -> Void
21+
-- f a = g -> Void
22+
-- g a = (a -> Void) -> Void
23+
-- g a = doubleNeg a
24+
-- f a = (doubleNeg) -> Void
25+
reduceTripleNeg :: Not (Not (Not a)) -> Not a
26+
reduceTripleNeg f a = f (doubleNeg a)

haskell/hw0/src/HW0/T3.hs

+82
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
module HW0.T3 (s, k, i, compose, contract, permute) where
2+
3+
-- s :: (a -> b -> c) -> (a -> b) -> (a -> c)
4+
-- f = (a -> b -> c)
5+
-- g = (a -> b)
6+
-- x = a
7+
-- f x (g x) = f a b = c
8+
s :: (a -> b -> c) -> (a -> b) -> (a -> c)
9+
s f g x = f x (g x)
10+
11+
k :: a -> b -> a
12+
k x _ = x
13+
14+
-- i :: a -> a
15+
-- s k = (a=a -> b=b -> c=a) -> (a -> b) -> (a -> a)
16+
-- s k = (a -> b) -> (a -> a)
17+
-- s k k = (a=a -> b=b->a) -> (a -> a)
18+
-- s k k = a -> a
19+
i :: a -> a
20+
i = s k k
21+
22+
-- compose :: (b -> c) -> (a -> b) -> (a -> c)
23+
-- x = b -> c
24+
-- y = a -> b
25+
-- (x (y a)) -> ret c
26+
-- compose x y a = x (y a)
27+
-- no parameters allowed, try again!
28+
-- x = b -> c
29+
-- y = a -> b
30+
-- z = a
31+
-- k = a -> b -> a
32+
-- s = (a -> b -> c) -> (a -> b) -> (a -> c)
33+
-- k s = a={(a->b->c)->(a->b)->(a->c)} -> b -> a
34+
-- k s = b' -> (a -> b -> c) -> (a -> b) -> (a -> c)
35+
-- s (k s) = (a={b'} -> b={(a->b->c)} -> c={(a->b)->(a->c)}) -> (a -> b) -> (a -> c)
36+
-- s (k s) = (b' -> a -> b -> c) -> b' -> (a -> b) -> (a -> c)
37+
-- s (k s) = (b' -> a -> (b -> c)) -> b' -> (a -> b) -> (a -> c)
38+
-- s (k s) k = (b'={a2} -> a={b2} -> (b -> c)={a2}) -> b' -> (a -> b) -> (a -> c)
39+
-- s (k s) k = (b -> c) -> (b2 -> b) -> (b2 -> c)
40+
-- this is it.
41+
compose :: (b -> c) -> (a -> b) -> (a -> c)
42+
compose = s (k s) k
43+
44+
-- contract :: (a -> a -> b) -> (a -> b)
45+
-- x = a -> a -> b
46+
-- (x a a) = b
47+
-- contract f a = f a a
48+
-- try again, but without parameters
49+
-- k = a -> b -> a
50+
-- s = (a -> b -> c) -> (a -> b) -> (a -> c)
51+
-- s s = (a=(a2->b2->c2) -> b=(a2->b2) -> c=(a2->c2)) -> (a -> b) -> (a -> c)
52+
-- s s = ((a2 -> b2 -> c2) -> (a2 -> b2)) -> ((a2 -> b2 -> c2) -> (a2 -> c2))
53+
-- s s = ((a2 -> b2 -> c2) -> a2 -> b2) -> (a2 -> b2 -> c2) -> (a2 -> c2)
54+
-- s k = (a -> b) -> (a -> a)
55+
-- s k = (a -> b) -> a -> a
56+
-- s s (s k) = ((a2 -> b2 -> c2)={a->b} -> a2={a} -> b2={a}) -> (a2 -> b2 -> c2) -> (a2 -> c2)
57+
-- s s (s k) = ((a2={a} -> (b2 -> c2)={b}) -> a2={a} -> b2={a}) -> (a2 -> b2 -> c2) -> (a2 -> c2)
58+
-- s s (s k) = (a -> a -> c2) -> (a -> c2)
59+
contract :: (a -> a -> b) -> (a -> b)
60+
contract = s s (s k)
61+
62+
-- permute :: (a -> b -> c) -> (b -> a -> c)
63+
-- x = a -> b -> c
64+
-- y = b -> a -> c
65+
-- k = a -> b -> a
66+
-- s = (a -> b -> c) -> (a -> b) -> (a -> c)
67+
-- compose = (b -> c) -> (a -> b) -> (a -> c)
68+
-- k k = a={a2 -> b2 -> a2} -> b -> a
69+
-- k k = b -> a2 -> b2 -> a2
70+
-- k compose = a={(b2 -> c2) -> (a2 -> b2) -> (a2 -> c2)} -> b -> a
71+
-- k compose = b -> (b2 -> c2) -> (a2 -> b2) -> (a2 -> c2)
72+
-- s (k compose) = (a={b1} -> b={b2 -> c2} -> c={(a2 -> b2) -> (a2 -> c2)}) -> (a -> b) -> (a -> c)
73+
-- s (k compose) = (b1 -> b2 -> c2) -> b1 -> (a2 -> b2) -> a2 -> c2
74+
-- s (k compose) s = (b1={a -> b -> c} -> b2={a -> b} -> c2={a -> c}) -> b1 -> (a2 -> b2) -> a2 -> c2
75+
-- s (k compose) s = (a -> b -> c) -> (a2 -> a -> b) -> a2 -> a -> c
76+
-- s (s (k compose) s) = (a={a1 -> b1 -> c1} -> b={a2 -> a1 -> b1} -> c={a2 -> a1 -> c1}) -> (a -> b) -> (a -> c)
77+
-- s (s (k compose) s) = ((a1 -> b1 -> c1) -> a2 -> a1 -> b1) -> (a1 -> b1 -> c1) -> a2 -> a1 -> c1
78+
-- s (s (k compose) s) (k k) = ((a1 -> b1 -> c1) -> a2 -> a1 -> b1)={b -> a -> b' -> a} -> (a1 -> b1 -> c1) -> a2 -> a1 -> c1
79+
-- s (s (k compose) s) (k k) = ((a1 -> b1 -> c1)={b} -> a2={a} -> a1={b'} -> b1={a}) -> (a1 -> b1 -> c1) -> a2 -> a1 -> c1
80+
-- s (s (k compose) s) (k k) = (b' -> a -> c) -> a -> b' -> c
81+
permute :: (a -> b -> c) -> (b -> a -> c)
82+
permute = s (s (k (s (k s) k)) s) (k k)

haskell/hw0/src/HW0/T4.hs

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
module HW0.T4 (repeat', map', fib, fac) where
2+
3+
import Data.Function (fix)
4+
import Numeric.Natural (Natural)
5+
6+
-- fix: (a -> a) -> a
7+
-- fix f = {let x = f x} in x
8+
9+
-- x = f x
10+
-- x = f (f x)
11+
-- x = f (f (f x))
12+
-- oh, pretty recursion
13+
14+
repeat' :: a -> [a] -- behaves like Data.List.repeat
15+
repeat' = fix . (:)
16+
17+
map' :: (a -> b) -> [a] -> [b] -- behaves like Data.List.map
18+
map' f =
19+
fix
20+
( \rec list -> case list of
21+
(x : xs) -> f x : rec xs
22+
[] -> []
23+
)
24+
25+
fib :: Natural -> Natural -- computes the n-th Fibonacci number
26+
fib = fix (\rec a b depth -> if depth == 0 then a else rec b (a + b) (depth - 1)) 0 1
27+
28+
fac :: Natural -> Natural -- computes the factorial
29+
fac = fix (\rec n -> if n == 0 then 1 else n * rec (n - 1))

haskell/hw0/src/HW0/T5.hs

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
module HW0.T5 (Nat, nz, ns, nplus, nmult, nFromNatural, nToNum) where
2+
3+
import GHC.Natural (Natural)
4+
5+
-- Church numerals
6+
type Nat a = (a -> a) -> a -> a
7+
8+
-- (a -> a) -> a -> a == (a -> a) -> (a -> a)
9+
10+
nz :: Nat a
11+
nz _ a = a
12+
13+
-- ns :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
14+
-- n = ((a -> a) -> a -> a)
15+
-- f = (a -> a)
16+
-- x = a
17+
-- return a
18+
ns :: Nat a -> Nat a
19+
ns n f x = f $ n f x
20+
21+
nplus :: Nat a -> Nat a -> Nat a
22+
nplus n m f x = n f $ m f x
23+
24+
--nmult n m f = n $ m f
25+
--nmult n m f = n . m $ f
26+
--nmult n m = n . m
27+
--oops :D
28+
nmult :: Nat a -> Nat a -> Nat a
29+
nmult = (.)
30+
31+
nFromNatural :: Natural -> Nat a
32+
nFromNatural 0 = nz
33+
nFromNatural n = \f x -> f (nFromNatural (n - 1) f x)
34+
35+
nToNum :: Num a => Nat a -> a
36+
nToNum f = f (+ 1) 0 -- do +1 n times

0 commit comments

Comments
 (0)