Transcript
Die Programmiersprache Clean und Uniqueness Typing Julian Biendarra Fortgeschrittene Konzepte der funktionalen Programmierung Sommersemester 2015 TU München
27. Mai 2015
Abbildung: http://xkcd.com/1312
Clean
Abbildung: http://xkcd.com/1312
Gliederung 1
Hello World!
2
Clean
3
Syntax-Vergleich Haskell ↔ Clean
4
Uniqueness Typing Referenzielle Transparenz Einführung Theorie
5
Uniqueness Typing in Clean Attribute und Variablen Propagation Curried Funktionsanwendung
6
I/O in Clean Beispiel Hash Lets Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
3 / 26
Gliederung 1
Hello World!
2
Clean
3
Syntax-Vergleich Haskell ↔ Clean
4
Uniqueness Typing Referenzielle Transparenz Einführung Theorie
5
Uniqueness Typing in Clean Attribute und Variablen Propagation Curried Funktionsanwendung
6
I/O in Clean Beispiel Hash Lets Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
4 / 26
Hello World!
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
5 / 26
Hello World! Hello World in Haskell module Main where
Hello World in Clean module helloworld
main :: IO () main = putStr "Hello World!\n"
Start :: String Start = "Hello World!\n"
Hello World with Clean I/O module helloworldlong import StdEnv Start :: ∗ World -> ∗ World Start filesys0 | closeok = filesys2 | otherwise = abort "I/O Error" where (console, filesys1) = stdio filesys0 console1 = fwrites ("Hello World!\n") console (closeok, filesys2) = fclose console1 filesys1 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
5 / 26
Hello World! Hello World in Haskell module Main where
Hello World in Clean module helloworld
main :: IO () main = putStr "Hello World!\n"
Start :: String Start = "Hello World!\n"
Hello World with Clean I/O module helloworldlong import StdEnv Start :: ∗ World -> ∗ World Start filesys0 | closeok = filesys2 | otherwise = abort "I/O Error" where (console, filesys1) = stdio filesys0 console1 = fwrites ("Hello World!\n") console (closeok, filesys2) = fclose console1 filesys1 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
5 / 26
Hello World! Hello World in Haskell module Main where
Hello World in Clean module helloworld
main :: IO () main = putStr "Hello World!\n"
Start :: String Start = "Hello World!\n"
Hello World with Clean I/O module helloworldlong import StdEnv Start :: ∗ World -> ∗ World Start filesys0 | closeok = filesys2 | otherwise = abort "I/O Error" where (console, filesys1) = stdio filesys0 console1 = fwrites ("Hello World!\n") console (closeok, filesys2) = fclose console1 filesys1 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
5 / 26
Gliederung 1
Hello World!
2
Clean
3
Syntax-Vergleich Haskell ↔ Clean
4
Uniqueness Typing Referenzielle Transparenz Einführung Theorie
5
Uniqueness Typing in Clean Attribute und Variablen Propagation Curried Funktionsanwendung
6
I/O in Clean Beispiel Hash Lets Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
6 / 26
Clean http://clean.cs.ru.nl/Clean
rein funktionale Programmiersprache entwickelt 1984 an der University of Nijmegen basiert auf Manipulation von Graphen (sog. Term Graph Rewriting Systems)
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
7 / 26
Gliederung 1
Hello World!
2
Clean
3
Syntax-Vergleich Haskell ↔ Clean
4
Uniqueness Typing Referenzielle Transparenz Einführung Theorie
5
Uniqueness Typing in Clean Attribute und Variablen Propagation Curried Funktionsanwendung
6
I/O in Clean Beispiel Hash Lets Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
8 / 26
Syntax-Vergleich Haskell ↔ Clean
Fibonacci-Zahlen fib fib fib fib
:: Int -> Int 0 = 0 1 = 1 n = fib (n − 1) + fib (n − 2)
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
9 / 26
Syntax-Vergleich Haskell ↔ Clean
Fibonacci-Zahlen Haskell/Clean fib :: Int -> Int fib 0 = 0 fib 1 = 1 fib n = fib (n − 1) + fib (n − 2)
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
9 / 26
Syntax-Vergleich Haskell ↔ Clean Mehrere Funktionsparameter Haskell add :: Int -> Int -> Int add a b = a + b
Clean add :: Int Int -> Int add a b = a + b
Typklassen Haskell max :: (Ord a) => a -> a -> a Clean max :: a a -> a | Ord a Haskell sum :: (Num a) => [a] -> a sum [] = 0 sum (x:xs) = x + sum xs Julian Biendarra
Clean sum :: [a] -> a | +, zero a sum [] = zero sum [x:xs] = x + sum xs
Clean & Uniqueness Typing
27. Mai 2015
10 / 26
Syntax-Vergleich Haskell ↔ Clean Mehrere Funktionsparameter Haskell add :: Int -> Int -> Int add a b = a + b
Clean add :: Int Int -> Int add a b = a + b
Typklassen Haskell max :: (Ord a) => a -> a -> a Clean max :: a a -> a | Ord a Haskell sum :: (Num a) => [a] -> a sum [] = 0 sum (x:xs) = x + sum xs Julian Biendarra
Clean sum :: [a] -> a | +, zero a sum [] = zero sum [x:xs] = x + sum xs
Clean & Uniqueness Typing
27. Mai 2015
10 / 26
Syntax-Vergleich Haskell ↔ Clean Mehrere Funktionsparameter Haskell add :: Int -> Int -> Int add a b = a + b
Clean add :: Int Int -> Int add a b = a + b
Typklassen Haskell max :: (Ord a) => a -> a -> a Clean max :: a a -> a | Ord a Haskell sum :: (Num a) => [a] -> a sum [] = 0 sum (x:xs) = x + sum xs Julian Biendarra
Clean sum :: [a] -> a | +, zero a sum [] = zero sum [x:xs] = x + sum xs
Clean & Uniqueness Typing
27. Mai 2015
10 / 26
Gliederung 1
Hello World!
2
Clean
3
Syntax-Vergleich Haskell ↔ Clean
4
Uniqueness Typing Referenzielle Transparenz Einführung Theorie
5
Uniqueness Typing in Clean Attribute und Variablen Propagation Curried Funktionsanwendung
6
I/O in Clean Beispiel Hash Lets Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
11 / 26
Referenzielle Transparenz engl. referential transparency
Der gleiche Ausdruck muss bei jeder Auswertung das gleiche Ergebnis haben.
Funktion inc int inc(int n) { return n + 1; }
Beispiel inc(3) > 4 inc2(3) > 4
int one = 1;
one = 2 inc(3) > 4 inc2(3) > 5
int inc2(int n) { return n + one; }
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
12 / 26
Referenzielle Transparenz engl. referential transparency
Der gleiche Ausdruck muss bei jeder Auswertung das gleiche Ergebnis haben.
Funktion inc int inc(int n) { return n + 1; }
Beispiel inc(3) > 4 inc2(3) > 4
int one = 1;
one = 2 inc(3) > 4 inc2(3) > 5
int inc2(int n) { return n + one; }
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
12 / 26
Referenzielle Transparenz engl. referential transparency
Der gleiche Ausdruck muss bei jeder Auswertung das gleiche Ergebnis haben.
Funktion inc int inc(int n) { return n + 1; }
Beispiel inc(3) > 4 inc2(3) > 4
int one = 1;
one = 2 inc(3) > 4 inc2(3) > 5
int inc2(int n) { return n + one; }
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
12 / 26
Uniqueness Typing Referenzielle Transparenz erfüllt? int fget2c(FILE∗ file) { int a = fgetc(file); int b = fgetc(file); return a + b; } zu schützende Variablen werden als unique bezeichnet unique Variablen dürfen max. 1 Referenz auf sich haben Referenzielle Transparenz erfüllt? fget2c :: ∗ File -> (Int, ∗ File) fget2c file0 = let (a, file1) = fgetc file0 (b, file2) = fgetc file1 in (a + b, file2) Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
13 / 26
Uniqueness Typing Referenzielle Transparenz erfüllt? Nein! int fget2c(FILE∗ file) { int a = fgetc(file); int b = fgetc(file); return a + b; } zu schützende Variablen werden als unique bezeichnet unique Variablen dürfen max. 1 Referenz auf sich haben Referenzielle Transparenz erfüllt? fget2c :: ∗ File -> (Int, ∗ File) fget2c file0 = let (a, file1) = fgetc file0 (b, file2) = fgetc file1 in (a + b, file2) Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
13 / 26
Uniqueness Typing Referenzielle Transparenz erfüllt? Nein! int fget2c(FILE∗ file) { int a = fgetc(file); int b = fgetc(file); return a + b; } zu schützende Variablen werden als unique bezeichnet unique Variablen dürfen max. 1 Referenz auf sich haben Referenzielle Transparenz erfüllt? fget2c :: ∗ File -> (Int, ∗ File) fget2c file0 = let (a, file1) = fgetc file0 (b, file2) = fgetc file1 in (a + b, file2) Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
13 / 26
Uniqueness Typing Referenzielle Transparenz erfüllt? Nein! int fget2c(FILE∗ file) { int a = fgetc(file); int b = fgetc(file); return a + b; } zu schützende Variablen werden als unique bezeichnet unique Variablen dürfen max. 1 Referenz auf sich haben Referenzielle Transparenz erfüllt? fget2c :: ∗ File -> (Int, ∗ File) fget2c file0 = let (a, file1) = fgetc file0 (b, file2) = fgetc file1 in (a + b, file2) Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
13 / 26
Uniqueness Typing Referenzielle Transparenz erfüllt? Nein! int fget2c(FILE∗ file) { int a = fgetc(file); int b = fgetc(file); return a + b; } zu schützende Variablen werden als unique bezeichnet unique Variablen dürfen max. 1 Referenz auf sich haben Referenzielle Transparenz erfüllt? Ja! fget2c :: ∗ File -> (Int, ∗ File) fget2c file0 = let (a, file1) = fgetc file0 (b, file2) = fgetc file1 in (a + b, file2) Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
13 / 26
Uniqueness Typing Referenzielle Transparenz erfüllt? Nein! int fget2c(FILE∗ file) { int a = fgetc(file); int b = fgetc(file); return a + b; } zu schützende Variablen werden als unique bezeichnet unique Variablen dürfen max. 1 Referenz auf sich haben
fget2c :: ∗ File -> (Int, ∗ File) fget2c file0 = let (a, file1) = fgetc file0 (b, file2) = fgetc file0 in (a + b, file2) Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
13 / 26
Uniqueness Typing Referenzielle Transparenz erfüllt? Nein! int fget2c(FILE∗ file) { int a = fgetc(file); int b = fgetc(file); return a + b; } zu schützende Variablen werden als unique bezeichnet unique Variablen dürfen max. 1 Referenz auf sich haben Uniqueness von file0 verletzt! fget2c :: ∗ File -> (Int, ∗ File) fget2c file0 = let (a, file1) = fgetc file0 (b, file2) = fgetc file0 in (a + b, file2) Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
13 / 26
Uniqueness als Attribut
Uniqueness als Attribut des Typs einer Variable: Notation non-unique unique
vereinfacht [11] type× type•
Clean type ∗ type
Uniqueness-Variable
typeu
u:type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel × w const :: t u −→ s v −→ t u [w ≤ u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
14 / 26
Uniqueness als Attribut
Uniqueness als Attribut des Typs einer Variable: Notation non-unique unique
vereinfacht [11] type× type•
Clean type ∗ type
Uniqueness-Variable
typeu
u:type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel × w const :: t u −→ s v −→ t u [w ≤ u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
14 / 26
Uniqueness als Attribut
Uniqueness als Attribut des Typs einer Variable: Notation non-unique unique
vereinfacht [11] type× type•
Clean type ∗ type
Uniqueness-Variable
typeu
u:type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel × w const :: t u −→ s v −→ t u [w ≤ u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
14 / 26
Uniqueness als Attribut
Uniqueness als Attribut des Typs einer Variable: Notation non-unique unique
vereinfacht [11] type× type•
Clean type ∗ type
Uniqueness-Variable
typeu
u:type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel × w const :: t u −→ s v −→ t u [w ≤ u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
14 / 26
Uniqueness als Attribut
Uniqueness als Attribut des Typs einer Variable: Notation non-unique unique
vereinfacht [11] type× type•
Clean type ∗ type
Uniqueness-Variable
typeu
u:type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel × w const :: t u −→ s v −→ t u [w ≤ u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
14 / 26
Uniqueness-Attribut als Typ
Idee: • und × sind Typen wie Int Char Problem: Was ist ein Wert vom Typ •? Lösung:
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
15 / 26
Uniqueness-Attribut als Typ
Idee: • und × sind Typen wie Int Char Problem: Was ist ein Wert vom Typ •? Lösung:
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
15 / 26
Uniqueness-Attribut als Typ
Idee: • und × sind Typen wie Int Char Problem: Was ist ein Wert vom Typ •? Lösung: Kinds sind die „Typen der Typen“ ∗ konkreter Typ T Typ ohne Uniqueness-Attribut U Uniqueness-Attribut: • oder × Attr :: T -> U -> ∗
Julian Biendarra
konstruiert konkrete Typen
Clean & Uniqueness Typing
27. Mai 2015
15 / 26
Uniqueness-Attribut als Typ
Idee: • und × sind Typen wie Int Char Problem: Was ist ein Wert vom Typ •? Lösung: Kinds sind die „Typen der Typen“ ∗ konkreter Typ T Typ ohne Uniqueness-Attribut U Uniqueness-Attribut: • oder × Attr :: T -> U -> ∗
Julian Biendarra
konstruiert konkrete Typen
Clean & Uniqueness Typing
27. Mai 2015
15 / 26
Uniqueness-Attribut als Typ
Idee: • und × sind Typen wie Int Char Problem: Was ist ein Wert vom Typ •? Lösung: Kinds sind die „Typen der Typen“ ∗ konkreter Typ T Typ ohne Uniqueness-Attribut U Uniqueness-Attribut: • oder × Attr :: T -> U -> ∗
Julian Biendarra
konstruiert konkrete Typen
Clean & Uniqueness Typing
27. Mai 2015
15 / 26
Uniqueness-Attribut als Typ
Idee: • und × sind Typen wie Int Char Problem: Was ist ein Wert vom Typ •? Lösung: Kinds sind die „Typen der Typen“ ∗ konkreter Typ T Typ ohne Uniqueness-Attribut U Uniqueness-Attribut: • oder × Attr :: T -> U -> ∗
Julian Biendarra
konstruiert konkrete Typen
Clean & Uniqueness Typing
27. Mai 2015
15 / 26
Uniqueness-Attribut als Typ
Idee: • und × sind Typen wie Int Char Problem: Was ist ein Wert vom Typ •? Lösung: Kinds sind die „Typen der Typen“ ∗ konkreter Typ T Typ ohne Uniqueness-Attribut U Uniqueness-Attribut: • oder × Attr :: T -> U -> ∗
Julian Biendarra
konstruiert konkrete Typen
Clean & Uniqueness Typing
27. Mai 2015
15 / 26
Uniqueness-Attribut als Typ
Idee: • und × sind Typen wie Int Char Problem: Was ist ein Wert vom Typ •? Lösung: Kinds sind die „Typen der Typen“ ∗ konkreter Typ T Typ ohne Uniqueness-Attribut U Uniqueness-Attribut: • oder × Attr :: T -> U -> ∗
Julian Biendarra
konstruiert konkrete Typen
Clean & Uniqueness Typing
27. Mai 2015
15 / 26
Gliederung 1
Hello World!
2
Clean
3
Syntax-Vergleich Haskell ↔ Clean
4
Uniqueness Typing Referenzielle Transparenz Einführung Theorie
5
Uniqueness Typing in Clean Attribute und Variablen Propagation Curried Funktionsanwendung
6
I/O in Clean Beispiel Hash Lets Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
16 / 26
Uniqueness-Attribute und -Variablen Notation non-unique unique necessarily unique
vereinfacht [11] type× type• –
Clean type ∗ type ∗ type
Uniqueness-Variable anonyme Uniqueness-Variable
typeu –
u:type .type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel const :: u:t -> w:(v:s -> u:t), [w <= u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
17 / 26
Uniqueness-Attribute und -Variablen Notation non-unique unique necessarily unique
vereinfacht [11] type× type• –
Clean type ∗ type ∗ type
Uniqueness-Variable anonyme Uniqueness-Variable
typeu –
u:type .type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel const :: u:t -> w:(v:s -> u:t), [w <= u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
17 / 26
Uniqueness-Attribute und -Variablen Notation non-unique unique necessarily unique
vereinfacht [11] type× type• –
Clean type ∗ type ∗ type
Uniqueness-Variable anonyme Uniqueness-Variable
typeu –
u:type .type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel const :: u:t -> w:(v:s -> u:t), [w <= u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
17 / 26
Uniqueness-Attribute und -Variablen Notation non-unique unique necessarily unique
vereinfacht [11] type× type• –
Clean type ∗ type ∗ type
Uniqueness-Variable anonyme Uniqueness-Variable
typeu –
u:type .type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel const :: u:t -> w:(v:s -> u:t), [w <= u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
17 / 26
Uniqueness-Attribute und -Variablen Notation non-unique unique necessarily unique
vereinfacht [11] type× type• –
Clean type ∗ type ∗ type
Uniqueness-Variable anonyme Uniqueness-Variable
typeu –
u:type .type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel const :: u:t -> w:(v:s -> u:t), [w <= u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
17 / 26
Uniqueness-Attribute und -Variablen Notation non-unique unique necessarily unique
vereinfacht [11] type× type• –
Clean type ∗ type ∗ type
Uniqueness-Variable anonyme Uniqueness-Variable
typeu –
u:type .type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel const :: u:t -> w:(v:s -> u:t), [w <= u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
17 / 26
Uniqueness-Attribute und -Variablen Notation non-unique unique necessarily unique
vereinfacht [11] type× type• –
Clean type ∗ type ∗ type
Uniqueness-Variable anonyme Uniqueness-Variable
typeu –
u:type .type
Uniqueness-Bedingung
[w ≤ u]
[w <= u]
Beispiel const :: u:t -> w:(v:s -> u:t), [w <= u]
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
17 / 26
Uniqueness Propagation
head head :: [∗ a] -> ∗ a head [x:xs] = x
heads heads :: [∗ a] -> (∗ a, ∗ a) heads list = (head list, head list)
Uniqueness von a verletzt a unique ⇒ [a] unique
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
18 / 26
Uniqueness Propagation
head head :: [∗ a] -> ∗ a head [x:xs] = x
heads heads :: [∗ a] -> (∗ a, ∗ a) heads list = (head list, head list)
Uniqueness von a verletzt a unique ⇒ [a] unique
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
18 / 26
Uniqueness Propagation
head head :: [∗ a] -> ∗ a head [x:xs] = x
heads heads :: [∗ a] -> (∗ a, ∗ a) heads list = (head list, head list)
Uniqueness von a verletzt a unique ⇒ [a] unique
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
18 / 26
Uniqueness Propagation
head head :: [∗ a] -> ∗ a head [x:xs] = x
heads heads :: [∗ a] -> (∗ a, ∗ a) heads list = (head list, head list)
Uniqueness von a verletzt a unique ⇒ [a] unique
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
18 / 26
Uniqueness Propagation
head head :: ∗ [∗ a] -> head [x:xs] = x
∗
a
heads heads :: [∗ a] -> (∗ a, ∗ a) heads list = (head list, head list)
Uniqueness von a verletzt a unique ⇒ [a] unique
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
18 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec :: Char
∗
File ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel somefile ::
∗
Julian Biendarra
File
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec :: Char
∗
File ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel somefile ::
∗
Julian Biendarra
File
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec ::
∗
File Char ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel somefile ::
∗
Julian Biendarra
File
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec ::
∗
File Char ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel fwritec somefile :: u:(Char ->
Julian Biendarra
∗
File)
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec ::
∗
File Char ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel fwritec somefile :: Char ->
Julian Biendarra
∗
File
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec ::
∗
File Char ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel fwritec somefile :: Char ->
Julian Biendarra
∗
File
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec ::
∗
File Char ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel writeParallel (fwritec somefile) :: (∗ File,
Julian Biendarra
Clean & Uniqueness Typing
∗
File)
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec ::
∗
File Char ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel (fwritec somefile 'a', fwritec somefile 'b')
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec ::
∗
File Char ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel (fwritec somefile 'a', fwritec somefile 'b')
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec ::
∗
File Char ->
∗
File
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel fwritec somefile :: u:(Char ->
Julian Biendarra
∗
File)
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Uniqueness bei curried Anwendung von Funktionen fwritec fwritec ::
∗
File ->
∗
(Char ->
∗
File)
writeParallel writeParallel :: (Char -> ∗ File) -> (∗ File, writeParallel f = (f 'a', f 'b')
∗
File)
Beispiel fwritec somefile :: u:(Char ->
Julian Biendarra
∗
File)
Clean & Uniqueness Typing
27. Mai 2015
19 / 26
Gliederung 1
Hello World!
2
Clean
3
Syntax-Vergleich Haskell ↔ Clean
4
Uniqueness Typing Referenzielle Transparenz Einführung Theorie
5
Uniqueness Typing in Clean Attribute und Variablen Propagation Curried Funktionsanwendung
6
I/O in Clean Beispiel Hash Lets Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
20 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf readCharList readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 | not readok = ([], file1) | otherwise = ([c : cs], file2) where (readok, c, file1) = freadc file0 (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf readCharList readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 | not readok = ([], file1) | otherwise = ([c : cs], file2) where (readok, c, file1) = freadc file0 (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf readCharList readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 | not readok = ([], file1) | otherwise = ([c : cs], file2) where (readok, c, file1) = freadc file0 (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf readCharList readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 | not readok = ([], file1) | otherwise = ([c : cs], file2) where (readok, c, file1) = freadc file0 (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf readCharList readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 | not readok = ([], file1) | otherwise = ([c : cs], file2) where (readok, c, file1) = freadc file0 (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf readCharList readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 | not readok = ([], file1) | otherwise = ([c : cs], file2) where (readok, c, file1) = freadc file0 (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf readCharList readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 | not readok = ([], file1) | otherwise = ([c : cs], file2) where (readok, c, file1) = freadc file0 (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf catFile catFile :: String ∗ env -> ∗ env | FileSystem env catFile filename filesys0 | readok && closeok0 && closeok1 = filesys4 | otherwise = abort "I/O Error" where (readok, file0, filesys1) = fopen filename FReadText filesys0 (charList, file1) = readCharList file0 (closeok0, filesys2) = fclose file1 filesys1 (console0, filesys3) = stdio filesys2 console1 = fwrites (toString charList) console0 (closeok1, filesys4) = fclose console1 filesys3 Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
I/O Beispiel: cat in Clean readCharList liest Datei als Liste von Chars ein catFile schreibt Inhalt von Datei auf stdout Start ruft catFile auf Start Start :: ∗ World -> ∗ World Start world = catFile "test.txt" world
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
21 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList ohne Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 | not readok = ([], file1) | otherwise = ([c : cs], file2) where (readok, c, file1) = freadc file0 (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList ohne Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 | not readok = ([], file1) | otherwise = ([c : cs], file2) where (readok, c, file1) = freadc file0 (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList mit Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 # (readok, c, file) = freadc file | not readok = ([], file1) | otherwise = ([c : cs], file2) where (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList mit Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 # (readok, c, file) = freadc file | not readok = ([], file1) | otherwise = ([c : cs], file2) where (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList mit Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 # (readok, c, file) = freadc file | not readok = ([], file) | otherwise = ([c : cs], file2) where (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList mit Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 # (readok, c, file) = freadc file | not readok = ([], file) | otherwise = ([c : cs], file2) where (cs, file2) = readCharList file1
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList mit Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 # (readok, c, file) = freadc file | not readok = ([], file) # (cs, file) = readCharList file | otherwise = ([c : cs], file2)
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList mit Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 # (readok, c, file) = freadc file | not readok = ([], file) # (cs, file) = readCharList file | otherwise = ([c : cs], file2)
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList mit Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 # (readok, c, file) = freadc file | not readok = ([], file) # (cs, file) = readCharList file | otherwise = ([c : cs], file)
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList mit Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file0 # (readok, c, file) = freadc file | not readok = ([], file) # (cs, file) = readCharList file | otherwise = ([c : cs], file)
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Hash Lets # x = x + 1 Syntactic Sugar für Definitionen mit where Scope: ab nächster Zeile über alle folgenden Hash Lets und Guards lesbarer Code (vergleichbar mit imperativen Programm)
readCharList mit Hash Lets readCharList :: ∗ File -> ([Char], ∗ File) readCharList file # (readok, c, file) = freadc file | not readok = ([], file) # (cs, file) = readCharList file | otherwise = ([c : cs], file)
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
22 / 26
Vielen Dank für eure Aufmerksamkeit!
module fragen Start :: String Start = "Fragen?\n"
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
23 / 26
Quellen I Achten, Peter: Clean for Haskell98 Programmers – A Quick Reference Guide. http://www.mbsd.cs.ru.nl/publications/papers/2007/ achp2007-CleanHaskellQuickGuide.pdf, 2007. Abgerufen am 09.05.2015. Achten, Peter und Martin Wierich: A Tutorial to the Clean Object I/O Library – Version 1.2. http: //clean.cs.ru.nl/download/supported/ObjectIO.1.2/doc/tutorial.pdf, 2004. Abgerufen am 17.04.2015. Barendsen, Erik und Sjaak Smetsers: Conventional and uniqueness typing in graph rewrite systems. In: Shyamasundar, Rudrapatna K. (Herausgeber): Foundations of Software Technology and Theoretical Computer Science, Band 761 der Reihe Lecture Notes in Computer Science, Seiten 41–51. Springer Berlin Heidelberg, 1993. Barendsen, Erik und Sjaak Smetsers: Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6:579–612, 1996.
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
24 / 26
Quellen II Brus, Tom, Marko van Eekelen, Maarten van Leer und Rinus Plasmeijer: Clean – A language for functional graph rewriting. In: Kahn, Gilles (Herausgeber): Functional Programming Languages and Computer Architecture, Band 274 der Reihe Lecture Notes in Computer Science, Seiten 364–384. Springer Berlin Heidelberg, 1987. Eekelen, Marko van, Sjaak Smetsers und Rinus Plasmeijer: Graph rewriting semantics for functional programming languages. In: Dalen, Dirk van und Marc Bezem (Herausgeber): Computer Science Logic, Band 1258 der Reihe Lecture Notes in Computer Science, Seiten 106–128. Springer Berlin Heidelberg, 1997. Koopman, Pieter: Functional Programming in Clean – An Appetizer. http://www.inf.ufsc.br/~jbosco/tutorial.html. Abgerufen am 17.04.2015. Koopman, Pieter, Rinus Plasmeijer, Marko van Eekelen und Sjaak Smetsers: Functional Programming in Clean. http://www.mbsd.cs.ru.nl/papers/cleanbook/CleanBookI.pdf, 2002. Part 1.
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
25 / 26
Quellen III
Plasmeijer, Rinus und Marko van Eekelen: Functional Programming and Parallel Graph Rewriting. Addison-Wesley, 1993. Plasmeijer, Rinus, Marko van Eekelen und John van Groningen: Clean language report – Version 2.2. http://clean.cs.ru.nl/download/doc/CleanLangRep.2.2.pdf, 2011. Abgerufen am 17.04.2015. Vries, Edsko de, Rinus Plasmeijer und David M. Abrahamson: Uniqueness Typing Simplified. In: Chitil, Olaf, Zoltán Horváth und Viktória Zsók (Herausgeber): Implementation and Application of Functional Languages, Band 5083 der Reihe Lecture Notes in Computer Science, Seiten 201–218. Springer Berlin Heidelberg, 2008.
Julian Biendarra
Clean & Uniqueness Typing
27. Mai 2015
26 / 26
