-- 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
--