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