Vorlesung: Praxis der Funktionalen Programmierung | Index

Realisierung von Funktionen

Der Gedanke des "immer neu Ausführens" ist interessant, weil wir auf diese Weise auch Abhängikeiten von anderen Bindungen benutzen können.

Erlaubt sein soll

let { f x = x + x } in f 0
Wir ändern dazu zunächst die abstrakte Syntax
module Function_Type 

where

import Op

data Term = Constant Integer
	  | Apply_Fun String [ Term ]
	  | Apply_Op  Op Term Term
	  | If Term Term Term
	  | Let [ (String, [String], Term) ] Term
     deriving Show




dann entsprechend deren grafische Darstellung (Quelltext) sowie schließlich die konkrete Syntax (den Parser) (Quelltext). Die wesentliche Änderung dabei ist, daß dort, wo wir früher nur einen Namen lasen, jetzt eine Folgen von Namen (links vom "=") bzw. ein Name und dann eine Folge von Termen erlaubt sind:
bindung :: Parser Term
bindung = do
    keyword "let"
    nts <- brace $ sepBy (operator ";")
		 $ do n <- name'
		      params <- many name'
		      operator "="
		      t <- term	
		      return (n, params, t)
    keyword "in"
    body <- term
    return $ Let nts body
Wir merken uns jetzt also in Let-Umgebungen nicht Bindungen der Variablen an fertige Werte, sondern an (unausgewertete) Terme, und zudem noch die Namen der formalen Parameter, damit wir beim Aufruf die passende Umgebung zusammensetzen können. Das sieht dann so aus:
module Function_Eval where

import Function_Type
import Function_Form
import Env
import Meaning

import MonadZero
import MonadPlus

import Prelude hiding (mapM)
import MapM

type Function = ([String], Term)

eval :: (MonadZero m, MonadPlus m) 
     => Envs Function -> Term -> m Integer
eval envs t = case t of

    Constant n  -> return n

    If c y n -> do x <- eval envs c
		   if 0 == x 
		      then eval envs y
		      else eval envs n

    Apply_Op o l r -> do let [mx, my] = map (eval envs) [l, r]
			 let f = meaning o
			 x <- mx; y <- my
			 f x y

    Apply_Fun f args -> case finds envs f of
		  Nothing -> error $ "Variable/Funktion " ++ f
				   ++ " nicht gebunden"
		  Just (params, body) -> 
		      if length params /= length args
		      then error $ "Funktionsaufruf mit falscher Argumentzahl"
		      else let act = mkEnv [ (p, ([], a))
					   | (p, a) <- zip params args ] 
			   in  eval (act : envs) body			 

    Let binds body ->
        let act = mkEnv [ (f, (ps, b)) | (f, ps, b) <- binds ]
	in  eval (act : envs) body

eval_top :: (MonadZero m, MonadPlus m) 
	 => Term -> m Integer
eval_top = eval nullEnvs



und jetzt haben wir die Äquivalenz zwischen
let { x = 3 | 4 } in x * x   und   (3|4) * (3|4)

Probleme mit der naiven Implementierung

Probieren wir mal
let { e n = n + 1; z n = e (e n) } in z 0
Warum stürzt das ab (d. h. bleibt klemmen)? Hat offenbar was mit der doppelten Benutzung des n zu tun. Das ist aber sehr ärgerlich, für uns als Mathematiker sollte es solche Beschränkungen nicht geben. Namen von rein lokalen Variablen sollten nichts an der Semantik ändern.

Sehen wir uns die Auswertung an:

z 0 [ z = \ n -> e (e n), e = \ n -> n + 1 ]
e (e n) [ n = 0, z = .., e = \ n -> n + 1 ]
n + 1 [ n = e n, n = 0, z = .., e = .. ]
n [ n = e n, n = 0, z = .., e = .. ]
e n [ n = e n, n = 0, z = .., e = \ n -> n + 1 ]
Hier ist es passiert: es hätte e 0 dort stehen sollen, aber die richtige Bindung ist verdeckt. Mit umbenannten Variablen geht es:
z 0 [ z = \ n -> e (e n), e = \ k -> k + 1 ]
e (e n) [ n = 0, z = .., e = \ k -> k + 1 ]
k + 1 [ k = e n, n = 0, z = .., e = .. ]
k [ k = e n, n = 0, z = .., e = .. ]
e n [ k = e n, n = 0, z = .., e = \ n -> n + 1 ]

Die Lösung: Statische Bindung

Nun wollen wir aber nicht bei jedem Aufruf umbenennen. Stattdessen merken wir uns bei jeder Funktionsbindung die Umgebung zum Definitionszeitpunkt (d. h. statisch) und schlagen die Werte der Variablen im Body dort (und nicht in der Aufrufumgebungsliste, d. h. dynamisch) nach.

Um das zu implementieren, müssen wir den Interpreter erweitern: nicht Function = ([String], Term), sondern Function = ([String], Term, Envs Function). Das geht aber mit Typ-Synonymen nicht (diese dürfen nicht rekursiv sein), sondern nur mit algebraischen Datentypen.

module Static_Eval where

-- Unterschiede zu   module Function_Eval 
-- (d. h. dynamische Bindung)
-- sind mit !!! markiert

import Function_Type
import Function_Form
import Env
import Meaning

import MonadZero
import MonadPlus

import Prelude hiding (mapM)
import MapM

-- !!!
data Function = Function ([String], Term, Envs Function)
     deriving Show

eval :: (MonadZero m, MonadPlus m) 
     => Envs Function -> Term -> m Integer
eval envs t = case t of

    Constant n  -> return n

    If c y n -> do x <- eval envs c
		   if 0 == x 
		      then eval envs y
		      else eval envs n

    Apply_Op o l r -> do let [mx, my] = map (eval envs) [l, r]
			 let f = meaning o
			 x <- mx; y <- my
			 f x y

    Apply_Fun f args -> case finds envs f of
		  Nothing -> error $ "Variable/Funktion " ++ f
				   ++ " nicht gebunden"
		  -- !!!
		  Just ( Function (params, body, static_envs) ) -> 
		      if length params /= length args
		      then error $ "Funktionsaufruf mit falscher Argumentzahl"
		      else let act = mkEnv [ (p, Function ([], a, envs)) 
					   | (p, a) <- zip params args ]
			   in  eval (act : static_envs) body 

    Let binds body ->
        let act = mkEnv [ (f, Function (ps, b, envs)) 
			| (f, ps, b) <- binds ]
	in  eval (act : envs) body

eval_top :: (MonadZero m, MonadPlus m) 
	 => Term -> m Integer
eval_top = eval nullEnvs



Rekursive Bindungen

Mit der statischen Bindung ist der oben gezeigte Fehler (Absturz) behoben, aber das System verhält sich immer noch nicht so, wie wir das erwartet haben (probiere das obige Beispiel direkt.) Wir müssen umschreiben
let { e n = n + 1} in let { z n = e (e n) } in z 0
denn die Bindungen innerhalb eines let sehen sich gegenseitig (und auch selbst) nicht. (Das wird es jetzt, bei der korrekten Implementierung, klar). Wir retten das wie folgt:
    Let binds body ->
        let act = mkEnv [ (f, Function (ps, b, envs')) 
			| (f, ps, b) <- binds ]
	    envs' = act : envs
	in  eval envs' body
Das sieht sehr nach "an den eigenen Haaren aus dem Sumpf ziehen" aus, ist aber gar nicht so schlimm: Haskell selbst hat wegen der lazy evaluation nichts gegen rekursive Bindungen.

best viewed with any browser


http://www.informatik.uni-leipzig.de/~joe/ mailto:joe@informatik.uni-leipzig.de