diff options
Diffstat (limited to 'ws2015/ffp/blaetter/11/FFP_U11-1_GADTs.hs')
-rw-r--r-- | ws2015/ffp/blaetter/11/FFP_U11-1_GADTs.hs | 115 |
1 files changed, 115 insertions, 0 deletions
diff --git a/ws2015/ffp/blaetter/11/FFP_U11-1_GADTs.hs b/ws2015/ffp/blaetter/11/FFP_U11-1_GADTs.hs new file mode 100644 index 0000000..495e4c5 --- /dev/null +++ b/ws2015/ffp/blaetter/11/FFP_U11-1_GADTs.hs | |||
@@ -0,0 +1,115 @@ | |||
1 | -- Fortgeschrittene Funktionale Programmierung, | ||
2 | -- LMU, TCS, Wintersemester 2015/16 | ||
3 | -- Steffen Jost, Alexander Isenko | ||
4 | -- | ||
5 | -- Übungsblatt 11. 13.01.2016 | ||
6 | -- | ||
7 | -- Thema: GADTs, Yesod-Formulare | ||
8 | -- | ||
9 | -- Hinweis: | ||
10 | -- Für Übung A11-2 und A11-3 benötigen Sie die Yesod-Bibliothek. | ||
11 | -- Hinweise zur Installation mit Stack finden sich in den Folien | ||
12 | -- und auf Alexander's githup Seite: | ||
13 | -- https://github.com/cirquit/ffp-lib | ||
14 | -- | ||
15 | -- Die Aufgaben A11-2 und A11-3 finden Sie in separaten, beiligenden Dateien. | ||
16 | -- Dies ist notwendig, weil sich sonst das von Yesod verwendete TemplateHaskell | ||
17 | -- in die Quere kommt. | ||
18 | |||
19 | {-# LANGUAGE GADTs #-} | ||
20 | |||
21 | module Main where | ||
22 | |||
23 | |||
24 | main :: IO () | ||
25 | main = main_A11_1 | ||
26 | |||
27 | |||
28 | |||
29 | -- A11-1 GADTs | ||
30 | -- | ||
31 | -- Ein beliebtes Beispiel für die Mächtigkeit von GADTs ist ein Datentyp | ||
32 | -- zur sicheren Verwendung von head und tail auf Listen. | ||
33 | -- | ||
34 | -- Betrachten Sie dazu folgende Datentypdeklarationen, | ||
35 | -- bei denen einen Listentyp SList a b deklariert wird, | ||
36 | -- dessen zweites Typargument protokolliert, ob die Liste | ||
37 | -- leer ist oder nicht: | ||
38 | |||
39 | -- We should call these "Z" and "S", they're peano naturals. | ||
40 | data Empty = Empty | ||
41 | data NonEmpty a = NonEmpty | ||
42 | |||
43 | data SList a b where | ||
44 | Nil :: SList a Empty | ||
45 | Cons :: a -> SList a b -> SList a (NonEmpty b) | ||
46 | |||
47 | list0 :: SList Int Empty | ||
48 | list0 = Nil | ||
49 | |||
50 | list1 :: SList Int (NonEmpty (NonEmpty Empty)) | ||
51 | list1 = Cons 42 (Cons 69 list0) | ||
52 | |||
53 | safeHead :: SList a (NonEmpty b) -> a | ||
54 | safeHead (Cons x _) = x | ||
55 | |||
56 | main_A11_1 :: IO () | ||
57 | main_A11_1 = do | ||
58 | putStrLn "Hallo zur Übung 10!" | ||
59 | -- print $ safeHead list0 -- Zeile 1: liefert Typfehler beim Kompilieren! | ||
60 | print $ safeHead list1 -- Zeile 2: sollte funktionieren | ||
61 | print $ safeHead $ safeTail list1 -- Zeile 3: sollte funktionieren | ||
62 | -- print $ safeHead $ safeTail $ safeTail list1 -- Zeile 4: sollte Typfehler beim Kompilieren liefern! | ||
63 | |||
64 | -- a) Machen Sie als Aufwärmübung den Datentyp SList | ||
65 | -- zu einer Instanz der Typklasse Show. | ||
66 | -- Zur vereinfachten Behandlung der Klammerung geben wir die Listen so aus: | ||
67 | -- > list0 | ||
68 | -- [] | ||
69 | -- > list1 | ||
70 | -- 42:69:[] | ||
71 | |||
72 | |||
73 | instance Show a => Show (SList a b) where | ||
74 | showsPrec _ Nil = showString "[]" | ||
75 | showsPrec d (Cons a as) = showParen (d > 10) $ showsPrec (10 + 1) a . showString ":" . showsPrec (10 + 1) as | ||
76 | |||
77 | |||
78 | -- b) Geben Sie den Typ von list1 explizit an! | ||
79 | |||
80 | |||
81 | -- !!! TODO !!! Typangabe | ||
82 | |||
83 | |||
84 | -- c) Wie wir mit Zeile 1 von main_A11_1 überprüfen können, | ||
85 | -- wird eine Aufruf von safeHead auf eine leere Liste | ||
86 | -- bereits während der Kompilation von der Typprüfung verhindert! | ||
87 | -- | ||
88 | -- Probieren Sie dies durch Entfernen der Kommentare in Zeile 1 von main_A11_1 aus, | ||
89 | -- und schauen Sie sich die Fehlermeldung an. Was passiert hier? | ||
90 | -- | ||
91 | -- Warum würde eine Datentypdeklaration wie | ||
92 | -- data IsEmpty a = Empty | NonEmpty a | ||
93 | -- anstatt von Empty und NonEmpty hier nicht weiterhelfen? | ||
94 | |||
95 | |||
96 | {- | ||
97 | A type like IsEmpty carries the sought after distinction at value level -- ordinary lists do so as well. | ||
98 | -} | ||
99 | |||
100 | |||
101 | -- d) Deklarieren Sie eine Funktion safeTail, | ||
102 | -- welche einer SList den Kopf entfernt. | ||
103 | -- Achten Sie dabei auf die korrekte Typsignatur! | ||
104 | -- Wenn Sie es richtig gemacht haben, dann sollte die | ||
105 | -- 3. Zeile von main_A11_1 sollte nun funktionieren | ||
106 | -- 4. Zeile von main_A11_1 einen Typfehler beim Kompilieren liefern | ||
107 | |||
108 | safeTail :: SList a (NonEmpty b) -> SList a b | ||
109 | safeTail (Cons _ l) = l | ||
110 | |||
111 | |||
112 | |||
113 | -- | ||
114 | -- Weiter geht es mit der Datei FFP_U11-2_Yesod.hs | ||
115 | -- | ||