Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2013 / Einführung in die Funktionale Programmierung / EFP Material / Codevorlage: A8-4 Unifikation II


Inhaltsbereich

Codevorlage: A8-4 Unifikation II

Codevorlage zur Hausaufgabe A8-4 "Unifikation II". Sie können diese Vorlage verwenden, aber Sie können auch ausschliesslich mit der Angabe aus dem Übungsblatt arbeiten.

Haskell source code icon Unifikation_Skeleton.hs — Haskell source code, 5 KB (5809 bytes)

Dateiinhalt

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
{-Diese Spracherweiterungen brauchen wir nur für die Definition der "Show TSub"-Typklasseninstanz.
  Es wurde ja die Frage gestellt, wie man Show-Instanzen zu Funktionstypen schreiben kann - also
  haben wir hier nun ein Beispiel dazu. Dies ist hier nur möglich, weil wir anstatt dem üblichen
        type Identifier = String 
  einen endlichen Datentyp verwendet haben (Identifier gehört zu den Typklassen Bounded und Enum).
  
  Wer die Spracherweiterungen nicht mag, kann auch die Instanzdeklaration durch eine Funktion
        showTSub :: TSub -> String
  ersetzen, und auf die Spracherweiterungen verzichten; showTSub muss dann explizit angewendet werden.
-}
data TTyp = TVar Identifier
          | TInt | TBool | TString 
          | TArrow TTyp TTyp
          | TListe TTyp            -- optional, ggf. alle 5 Zeilen mit TList auskommentieren
  deriving (Eq) -- Show-Instanz weiter unten von Hand deklariert
          
data Identifier = Alpha | Beta | Gamma | Delta
  deriving (Eq, Enum, Bounded)
  
type TSub = TTyp -> TTyp

type TEq  = (TTyp,TTyp)
                 
------------------------------------------------  
  

unifiziere :: [TEq]  -> TSub
unifiziere = -- TODO: implementieren Sie diese Funktion gemäß Vorlesungsfolie 08-S.48!
  error "Student hat unifiziere leider noch nicht implementiert!"
  
------------------------------------------------  
-- Hilfsfunktionen:

hasTVar :: Identifier -> TTyp -> Bool    -- Prüft ob Typvariable im Typ vorkommt
hasTVar var = has
  where -- Abkürzung "has", um nicht bei jedem rekursiven Aufruf jedes mal var übergeben zu müssen
    has :: TTyp -> Bool
    has (TVar v1)      = v1 == var
    has (TArrow t1 t2) = has t1 || has t2
    has (TListe t)     = has t
    has _othertype     = False

{- Alternative Definition ohne Hilfsfunktion:
hasTVar' :: Identifier -> TTyp -> Bool
hasTVar' var (TVar v1)      = v1 == var
hasTVar' var (TArrow t1 t2) = hasTVar' var t1 || hasTVar' var t2
hasTVar' var (TListe t)     = hasTVar' var t
hasTVar' var _othertype     = False  

GHC bietet für solche Datentypen auch ein generisches Fold an. Dazu muss man aber
ein paar Bibliotheken einbinden und den Typ TTyp parametrisieren, d.h. der Kopf
dieser Datei sollte dann so aussehen:

    {-#  LANGUAGE TypeSynonymInstances, FlexibleInstances, DeriveFoldable, DeriveFunctor #-}
    import qualified Data.Foldable as Fold
    import Data.Monoid

    type TTyp = TTyp' Identifier
    data TTyp' a = TVar a 
                | TInt | TBool | TString | TArrow (TTyp' a) (TTyp' a) | TListe (TTyp' a)
      deriving (Eq, Functor, Fold.Foldable)

    hasTVar :: Identifier -> TTyp -> Bool
    hasTVar var typ = getAny $ Fold.foldMap hasV typ
      where
        hasV :: Identifier -> Any
        hasV x = Any $ var == x
-}    

makeSubs    :: Identifier -> TTyp ->      TSub        -- makeSub alpa t erstellt [t/alpha]
-- makeSubs :: Identifier -> TTyp -> (TTyp -> TTyp)   -- Einsetzen des Typ-Synonyms kann zum Verständnis helfen?!
makeSubs var typ = applySub 
  where
    -- Wir kreieren die neue Substitution, in dem wir einfach zeigen, 
    -- wie diese neue Substitution angewendet wird:
    applySub :: TTyp -> TTyp
    applySub t1@(TVar v1)
      | v1 == var = typ
      | otherwise = t1
    applySub (TArrow t1 t2) 
      = TArrow (applySub t1) (applySub t2)
    applySub (TListe t1)    
      = TListe (applySub t1)                                
    applySub othertype      
      = othertype

------------------------------------      
-- Beispiele zum Testen, z.B. mit:
-- > unifiziere aufg1
-- 
alpha, beta, gamma, delta :: TTyp  
alpha = TVar Alpha
beta  = TVar Beta
gamma = TVar Gamma
delta = TVar Delta
  
aufg1, aufg2, aufg3, aufg4, aufg5, aufg6 :: [TEq]  

aufg1 = [(alpha `TArrow` beta, TInt `TArrow` beta)]

aufg2 =  [(alpha,beta),(beta,gamma)]

aufg3 = [(t1,t2)]
 where
   t1 = TArrow TInt  $ TArrow alpha beta
   t2 = TArrow alpha $ TArrow beta  TInt
   
aufg4 = [(t1,t2)]
 where
   t1 = alpha `TArrow` (alpha `TArrow` TInt)
   t2 = (TInt `TArrow` beta) `TArrow` beta
   
aufg5 =  [(t1,t2)]
 where
   t1 = alpha `TArrow` (alpha `TArrow` TInt)
   t2 = (TInt `TArrow` beta) `TArrow` gamma
   
aufg6 =  [(t1,t2)]
 where
   t1 = TInt `TArrow` alpha
   t2 = alpha `TArrow` TBool
  
-----------------------------------------------
-- Anzeige von TTyp und TSub


instance Show TTyp where -- etwas hübschere Show-Instanz als die automatisch generierte
{--- Herkömmliche Variante:
  show (TVar v)  = show v
  show (TInt)    = "Int"
  show (TBool)   = "Bool"
  show (TString) = "String"
  show (TArrow t1 t2) = "(" ++ (show t1) ++ ") -> " ++ (show t2)
  show (TListe t1)    = "[" ++ (show t1) ++ "]"              
  --
  -- Mit intelligenter Klammerung: -}
  showsPrec _ (TVar v)  = showsPrec 0 v
  showsPrec _ (TInt)    = showString "Bool"
  showsPrec _ (TBool)   = ("Int" ++) -- so kann man das auch schreiben
  showsPrec _ (TString) = showString "String"
  showsPrec n (t1 `TArrow` t2) = showParen (n>0) $ (showsPrec 1 t1) . showString " -> " . showsPrec 0 t2
  showsPrec _ (TListe t1)      = showString "[" . (showsPrec 0 t1) . showString "]"
  
  
instance Show Identifier where
  show Alpha = "a" -- "alpha"
  show Beta  = "b" -- "beta"
  show Gamma = "c" -- "gamma"
  show Delta = "d" -- "delta"

instance (Show (TTyp -> TTyp)) where -- geht nur gut, wenn wir alle Typvariablen kennen  
  show sigma = "[ "++ middle ++ " ]"
    where 
      middle = drop 3 $ concat $ map showTSub1 [minBound..maxBound]

      showTSub1 :: Identifier -> String
      showTSub1 v 
        | tv == tv' = "" -- etwas mit sich selbst zu ersetzen bringt keine Information
        | otherwise = ",  " ++ (show tv') ++ " / " ++ (show v)
        where 
          tv  = TVar v
          tv' = sigma tv  
         

Artikelaktionen

abgelegt unter:

Funktionsleiste