From a6f85b9b8894a7817baad1a5e850366d02eb197a Mon Sep 17 00:00:00 2001
From: Gregor Kleen <gkleen@yggdrasil.li>
Date: Wed, 13 Jan 2016 18:18:06 +0100
Subject: FFP 11.1

---
 ws2015/ffp/blaetter/11/FFP_U11-1_GADTs.hs | 115 ++++++++++++++++++++++++++++++
 1 file changed, 115 insertions(+)
 create mode 100644 ws2015/ffp/blaetter/11/FFP_U11-1_GADTs.hs

(limited to 'ws2015/ffp/blaetter/11/FFP_U11-1_GADTs.hs')

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 @@
+-- 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
+-- 
-- 
cgit v1.2.3