Fixes

thesis.bib

@@ -203,3 +203,11 @@
     publisher = {ACM},
     address = {New York, NY, USA},
 }
+
+
+@online{erlang-typespec,
+  author = {Ericsson AB},
+  title = {Erlang Typespec},
+  url = {http://erlang.org/doc/reference_manual/typespec.html},
+}
+

thesis.tex

@@ -264,7 +264,8 @@ $otp/lib/compiler/src/core\_parse.hrl$.
     \item Union
 \end{itemize}
 
-Οποιοσδήποτε όρος της Erlang μπορεί να αποτελέσει το περιεχόμενο των μηνυμάτων που ανταλλάσσουν διεργασίες μεταξύ τους.
+Οποιοσδήποτε όρος της Erlang μπορεί να αποτελέσει το περιεχόμενο των μηνυμάτων που ανταλλάσσουν διεργασίες μεταξύ τους
+\cite{erlang-typespec}.
 
 \section{Το εργαλείο Dialyzer}
 
@@ -281,12 +282,16 @@ $otp/lib/compiler/src/core\_parse.hrl$.
 είναι οι τύποι που πρέπει να έχουν οι συναρτήσεις (δηλαδή ο συνδυασμός των τύπων των ορισμάτων μιας συνάρτησης, και του
 τύπου του αποτελέσματος που αυτή η συνάρτηση επιστρέφει) προκειμένου να εξασφαλιστεί ότι η συνάρτηση δε θα παρουσιάσει κάποιο
 σφάλμα χρόνου εκτέλεσης που
-οφείλεται σε κάποια ασυνέπεια στους τύπους. Για παράδειγμα, στο κομμάτι κώδικα του σχήματος $2.1$ το να καλέσουμε τη συνάρτηση $foo/1$
+οφείλεται σε κάποια ασυνέπεια στους τύπους.
+
+Για παράδειγμα, στο κομμάτι κώδικα του σχήματος $2.1$ το να καλέσουμε τη συνάρτηση $foo/1$
 ως $foo("Hello")$ θα οδηγούσε σε σφάλμα χρόνου εκτέλεσης, καθώς ο τελεστής $+$ δε μπορεί να εφαρμοστεί σε ένα όρισμα
 τύπου $List$ σε Erlang. Αυτό οδηγεί το Dialyzer στο να συμπεραίνει τύπους με έναν συντηρητικό τρόπο:
 οι τύποι που κάνει assign σε συναρτήσεις, και οι οποίοι απορρέουν από τους τύπους που αποδίδει στα επιμέρους τμήματα δεδομένων στο
 σώμα των συναρτήσεων, αποτελούν ένα υπερσύνολο των
-πραγματικών τύπων των δεδομένων μιας συνάρτησης. Στο ίδιο κομμάτι κώδικα, ο τύπος που θα συμπέραινε ο Dialyzer για τη
+πραγματικών τύπων των δεδομένων μιας συνάρτησης.
+
+Στο ίδιο κομμάτι κώδικα, ο τύπος που θα συμπέραινε ο Dialyzer για τη
 συνάρτηση $foo/1$ είναι $Number \rightarrow Number$.
 
 \lstset{style=erlangCodeStyle}
@@ -299,11 +304,11 @@ $otp/lib/compiler/src/core\_parse.hrl$.
 εμφανίζονται μέσα στα σώματα των συναρτήσεων. Η έκδοση του Dialyzer που δημοσιεύεται ως μέρος του OTP δεν αποθηκεύει αυτήν την
 πληροφορία για όλη τη διάρκεια της ανάλυσης, αλλά μόνο για όσο χρειάζεται για την εκάστοτε συνάρτηση.
 Για τους σκοπούς της δικής μας ανάλυσης, χρειάζεται να γνωρίζουμε τους τύπους δεδομένων των Erlang terms σε κάθε γραμμή
-πηγαίου κώδικα ενός Erlang module. Προκειμένου να εξασφαλίσουμε αυτήν την πληροφορία, προβήκαμε στην τροποποίση του Dialyzer
+πηγαίου κώδικα ενός Erlang module. Προκειμένου να εξασφαλίσουμε αυτήν την πληροφορία, προβήκαμε στην τροποποίηση του Dialyzer
 με σκοπό την αποστολή της πληροφορίας τύπων δεδομένων στο σύστημά μας κατα τη διάρκεια της εκτέλεσης του dataflow analysis loop του.
 
 \section{Ταυτοχρονισμός σε Erlang}
-Ένα ισχυρό χαρακτηριστικό της Erlang είναι η υποστήριξη της για ταυτοχρονισμό. Παρέχει στον προγραμματιστή ένα σύνολο
+Ένα ισχυρό χαρακτηριστικό της Erlang είναι η εγγενής υποστήριξη της για ταυτοχρονισμό. Παρέχει στον προγραμματιστή ένα σύνολο
 από primitives για τη δημιουργία διεργασιών, και τη διαχείριση της επικοινωνίας μεταξύ αυτών. Αυτές δεν είναι διεργασίες
 σε επίπεδο λειτουργικού συστήματος, ούτε όμως και νήματα, αλλά αποτελούν οντότητες τις οποίες διαχειρίζεται
 η εικονική μηχανή εκτέλεσης της Erlang, ο BEAM.
@@ -313,7 +318,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
 είναι η ασύγχρονη ανταλλαγή μηνυμάτων. Κάθε διεργασία διαθέτει ένα "κουτί εισερχομένων", μια ουρά από μηνύματα που έχει λάβει από άλλες διεργασίες. Για να καταναλώσει
 ένα μήνυμα από αυτήν την ουρά, ο προγραμματιστής χρησιμοποιεί την έκφραση $receive$, με την οποία παίρνει ένα μήνυμα από
 την κεφαλή της ουράς, και το συγκρίνει με μια σειρά από
-μοτίβα (patterns) τα οποία αντιστοιχούνσ στα μηνύματα που περιμένει ότι το πρόγραμμά του θα λάβει στη συγκεκριμένη φάση
+μοτίβα (patterns) τα οποία αντιστοιχούν στα μηνύματα που περιμένει ότι το πρόγραμμά του θα λάβει στη συγκεκριμένη φάση
 της εκτέλεσης. Όταν μια σύγκριση πετύχει, η διεργασία συνεχίζει την εκτέλεσή της.
 
 \lstset{style=erlangCodeStyle}
@@ -337,7 +342,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
 ποτέ. Αντίστοιχα, αν καμία διεργασία δεν αποστείλει στη διεργασία που εκτελεί τον κώδικα του listing 2.2 κάποιο μήνυμα
 που να αντιστοιχεί σε ένα από τα μοτίβα της εντολής $receive$, η εκτέλεση θα "κρεμάσει" επ' αόριστον.
 Σε αυτήν την περίπτωση θα είχαμε ένα προβληματικό σενάριο, που
-προκύπτει από τη μη-συμμόρφωση ενός εκ των δύο μερών της επικοινωνίας στο αναμενόμενο πρωτόκολλο.
+προκύπτει από τη μη-συμμόρφωση τουλάχιστον ενός εκ των δύο μερών της επικοινωνίας στο αναμενόμενο πρωτόκολλο.
 
 %% Type and effect systems
 \chapter{Συστήματα τύπων και επιδράσεων}
@@ -345,7 +350,8 @@ $otp/lib/compiler/src/core\_parse.hrl$.
 Πολλές γλώσσες προγραμματισμού υλοποιούν ένα στατικό σύστημα τύπων, προκειμένου να εγγυηθούν ότι τελεστές εφαρμόζονται μόνο σε
 τελεσταίους της κατάλληλης μορφής, δηλαδή του κατάλληλου είδους \cite{types-and-prog-langs, advanced-types-and-prog-langs}. Για παράδειγμα, ένα κλασσικό σύστημα τύπων θα απέρριπτε
 το πρόγραμμα 3.1 (γραμμένο σε μια υποθετική γλώσσα), καθώς η πράξη της αφαίρεσης ($-$), δεν έχει νόημα όταν εφαρμόζεται
-σε μια συμβολοσειρά και έναν αριθμό (υποθέτουμε ότι η γλώσσα δεν παρέχει τη δυνατότητα υπερφόρτωσης τελεστών).
+σε μια συμβολοσειρά και έναν αριθμό (υποθέτουμε ότι η γλώσσα δεν παρέχει τη δυνατότητα υπερφόρτωσης τελεστών, με την
+οποία ένας προγραμματιστής θα μπορούσε να δώσει... νόημα σε αυτήν την πράξη).
 
 \begin{lstlisting}[caption=Ασύμβατοι Τελεσταίοι]
     begin
@@ -363,12 +369,14 @@ $otp/lib/compiler/src/core\_parse.hrl$.
 
 Προκειμένου να εξαλειφθεί η ανάγκη για τη χειρονακτική δήλωση των τύπων τμημάτων δεδομένων σε ένα πρόγραμμα,
 αναπτύχθηκαν συστήματα τύπων με αυτόματο συμπερασμό τύπων, όπως αυτό των Hindley-Milner (ή αλλιώς Dammas-Milner), με την
-γλώσσα ML να είναι η πρώτη που υλοποίησε ένα τέτοιο σύστημα.
+γλώσσα ML να είναι η πρώτη για την οποία υλοποιήθηκε ένα τέτοιο σύστημα.
 
 Η προσέγγιση των συστημάτων τύπων είναι να συσχετίζουν τύπους με προγράμματα. Οι τύποι περιγράφουν το είδος των δεδομένων
 τα οποία μεταχειρίζεται το πρόγραμμα. Ο συσχετισμός αυτός γίνεται μέσω ενός συνόλου κανόνων συμπερασμού, με βάση
 τη σύνταξη του προγράμματος, κάνοντας χρήση ενός περιβάλλοντος τύπων, το οποίο αντιστοιχεί τις ελεύθερες μεταβλητές ενός
-προγράμματος με τους τύπους τους. Η αντιστοίχηση αυτή εκφράζεται με μια σχέση του τύπου $ \Gamma |- e : \tau $, όπου:
+προγράμματος με τους τύπους τους.
+
+Η αντιστοίχηση αυτή εκφράζεται με μια σχέση του τύπου $ \Gamma \vdash e : \tau $, όπου:
 \begin{itemize}
     \item $\Gamma$ είναι το περιβάλλον τύπων
     \item $e$ είναι το πρόγραμμα υπό εξέταση
@@ -390,7 +398,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
 όπως:
 \begin{itemize}
         % FIXME bind-time <-> χρονος δεσίματος
-    \item Ανάλυση χρόνου δεσίματος, κατα την οποία προσπαθούμε να πραγματοποιήσουμε μια διάκριση ανάμεσα σε αυτά δεδομένα των
+    \item Ανάλυση χρόνου δεσίματος, κατα την οποία προσπαθούμε να πραγματοποιήσουμε μια διάκριση ανάμεσα σε αυτά τα δεδομένα των
         οποίων η τιμή είναι γνωστή κατα το χρόνο μεταγλώττισης (στατικά), και σε αυτά τα οποία αποκτούν τιμή κατα την
         εκτέλεση του προγράμματος (δυναμικά). Αυτού του τύπου η ανάλυση αποτελεί τη βάση της μερικής αποτίμησης που
         πραγματοποιούν μεταγλωττιστές
@@ -399,7 +407,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
         δε χρειάζεται να παράξει κώδικα για αυτήν. Επίσης, αν μια τιμή χρησιμοποιείται μόνο μια φορά, η μεταβλητή που
         την περιέχει μπορεί να συλλεγεί από τον συλλέκτη σκουπιδιών του περιβάλλοντος εκτέλεσης αμέσως μετά τη χρήση
         της.
-    \item Ανάλυση ροής ελέγχου, κατά την οποία προσπαθούμε, συνήθως σε γλώσσες με συναρτήσης υψηλότερης τάξης, να
+    \item Ανάλυση ροής ελέγχου, κατά την οποία προσπαθούμε, συνήθως σε γλώσσες με συναρτήσεις υψηλότερης τάξης, να
         συμπεράνουμε ποιες συναρτήσεις είναι πιθανοί "αποδέκτες" μιας κλήσης σε ένα πρόγραμμα, δηλαδή ποιες συναρτήσεις
         είναι πιθανό να αποκτήσουν τον ελέγχο ενός προγράμματος (το οποίο δεν είναι πάντα εμφανές σε γλώσσες τέτοιου
         τύπου από τον πηγαίο κώδικά τους).
@@ -413,10 +421,16 @@ $otp/lib/compiler/src/core\_parse.hrl$.
 αναφερθήκαμε παραπάνω, αλλά με μια διαφορά: οι ετικέτες σε αυτά τα συστήματα τύπων περιέχουν πληροφορία σχετικά με την
 συμπεριφορά του προγράμματος κατά τον χρόνο αποτίμησης και εκτέλεσής του.
 
-Σε ένα σύστημα τύπων και επιδράσεων, η αντιστοίχιση ενός προγράμματος με έναν τύπο και μια επίδραση γράφεται ως $ \Gamma |- e
+Σε ένα σύστημα τύπων και επιδράσεων, η αντιστοίχιση ενός προγράμματος με έναν τύπο και μια επίδραση γράφεται ως $ \Gamma
+\vdash e
 : \tau; \phi $, που σημαίνει ότι στο περιβάλλον $\Gamma$, το πρόγραμμα $e$ εμφανίζει μια επίδραση $\phi$, και εν τέλει επιστρέφει μια
 τιμή τύπου $\tau$.
 
+Ο αναγνώστης μπορεί να σκέφτεται τις επιδράσεις ενός προγράμματος σαν τις παρενέργειες που μπορεί να προκαλέσει στο
+περιβάλλον του σαν αποτέλεσμα της εκτέλεσής του. Για παράδειγμα, έχουν αναπτυχθεί συστήματα τύπων κι επιδράσεων που
+αντιμετωπίζουν τις προσβάσεις (εγγραφή και ανάγνωση) στη μνήμη από προγράμματα ως επιδράσεις των προγραμμάτων, τις
+οποίες και κωδικοποιούν \cite{advanced-types-and-prog-langs}.
+
 %% TODO simple type and effect system
 
 %% Session types