diff options
Diffstat (limited to 'doc/tutorial/gf-tutorial2.txt')
| -rw-r--r-- | doc/tutorial/gf-tutorial2.txt | 788 |
1 files changed, 785 insertions, 3 deletions
diff --git a/doc/tutorial/gf-tutorial2.txt b/doc/tutorial/gf-tutorial2.txt index 31622a62b..3df55e1e7 100644 --- a/doc/tutorial/gf-tutorial2.txt +++ b/doc/tutorial/gf-tutorial2.txt @@ -1894,14 +1894,796 @@ library. ===Dependent types=== -===Higher-order abstract syntax=== +**Dependent types** are a characteristic feature of GF, +inherited from the +**constructive type theory** of Martin-Löf and +distinguishing GF from most other grammar formalisms and +functional programming languages. +The initial main motivation for developing GF was, indeed, +to have a grammar formalism with dependent types. +As can be inferred from the fact that we introduce them only now, +after having written lots of grammars without them, +dependent types are no longer the only motivation for GF. +But they are still important and interesting. + + +Dependent types can be used for stating stronger +**conditions of well-formedness** than non-dependent types. +A simple example is postal addresses. Ignoring the other details, +let us take a look at addresses consisting of +a street, a city, and a country. +``` +abstract Address = { + cat + Address ; Country ; City ; Street ; + + fun + mkAddress : Country -> City -> Street -> Address ; + + UK, France : Country ; + Paris, London, Grenoble : City ; + OxfordSt, ShaftesburyAve, BdRaspail, RueBlondel, AvAlsaceLorraine : Street ; + } +``` +The linearization rules +are straightforward, +``` + lin + + mkAddress country city street = ss (street ++ "," ++ city ++ "," ++ country) ; + + UK = ss ("U.K.") ; + France = ss ("France") ; + Paris = ss ("Paris") ; + London = ss ("London") ; + Grenoble = ss ("Grenoble") ; + OxfordSt = ss ("Oxford" ++ "Street") ; + ShaftesburyAve = ss ("Shaftesbury" ++ "Avenue") ; + BdRaspail = ss ("boulevard" ++ "Raspail") ; + RueBlondel = ss ("rue" ++ "Blondel") ; + AvAlsaceLorraine = ss ("avenue" ++ "Alsace-Lorraine") ; +``` +with the exception of ``mkAddress``, where we have +reversed the order of the constituents. The type of ``mkAddress`` +in the abstract syntax takes its arguments in a "logical" order, +with increasing precision. (This order is sometimes even used in the concrete +syntax of addresses, e.g. in Russia). + + + +Both existing and non-existing addresses are recognized by this +grammar. The non-existing ones in the following randomly generated +list have afterwards been marked by *: +``` + > gr -cat=Address -number=7 | l + + * Oxford Street , Paris , France + * Shaftesbury Avenue , Grenoble , U.K. + boulevard Raspail , Paris , France + * rue Blondel , Grenoble , U.K. + * Shaftesbury Avenue , Grenoble , France + * Oxford Street , London , France + * Shaftesbury Avenue , Grenoble , France +``` +Dependent types provide a way to guarantee that addresses are +well-formed. What we do is to include **contexts** in +``cat`` judgements: +``` + cat Address ; + cat Country ; + cat City Country ; + cat Street (x : Country)(y : City x) ; +``` +The first two judgements are as before, but the third one makes +``City`` dependent on ``Country``: there are no longer just cities, +but cities of the U.K. and cities of France. The fourth judgement +makes ``Street`` dependent on ``City``; but since +``City`` is itself dependent on ``Country``, we must +include them both in the context, moreover guaranteeing that +the city is one of the given country. Since the context itself +is built by using a dependent type, we have to use variables +to indicate the dependencies. The judgement we used for ``City`` +is actually shorthand for +``` + cat City (x : Country) +``` +which is only possible if the subsequent context does not depend on ``x``. + +The ``fun`` judgements of the grammar are modified accordingly: +``` + fun + + mkAddress : (x : Country) -> (y : City x) -> Street x y -> Address ; + + UK : Country ; + France : Country ; + Paris : City France ; + London : City UK ; + Grenoble : City France ; + OxfordSt : Street UK London ; + ShaftesburyAve : Street UK London ; + BdRaspail : Street France Paris ; + RueBlondel : Street France Paris ; + AvAlsaceLorraine : Street France Grenoble ; +``` +Since the type of ``mkAddress`` now has dependencies among +its argument types, we have to use variables just like we used in +the context of ``Street`` above. What we claimed to be the +"logical" order of the arguments is now forced by the type system +of GF: a variable must be declared (=bound) before it can be +referenced (=used). -===Semantic definitions=== -===List categories=== +The effect of dependent types is that the *-marked addresses above are +no longer well-formed. What the GF parser actually does is that it +initially accepts them (by using a context-free parsing algorithm) +and then rejects them (by type checking). The random generator does not produce +illegal addresses (this could be useful in bulk mailing!). +The linearization algorithm does not care about type dependencies; +actually, since the //categories// (ignoring their arguments) +are the same in both abstract syntaxes, +we use the same concrete syntax +for both of them. +**Remark**. Function types //without// +variables are actually a shorthand notation: writing +``` + fun PredV1 : NP -> V1 -> S +``` +is shorthand for +``` + fun PredV1 : (x : NP) -> (y : V1) -> S +``` +or any other naming of the variables. Actually the use of variables +sometimes shortens the code, since we can write e.g. +``` + fun ConjNP : Conj -> (x,y : NP) -> NP ; + oper triple : (x,y,z : Str) -> Str = \x,y,z -> x ++ y ++ z ; +``` + + + +===Dependent types in syntax editing=== + +An extra advantage of dependent types is seen in +syntax editing: +when menus with possible refinements are created, +only those functions are shown that are type-correct. +For instance, if the editor state is +``` + mkAddress : Address + UK : Country + * ?2 : City UK + ?3 : Street UK ?2 +``` +only the cities of the U.K. are shown in the city menu. + +What is more, editing in the state +``` + mkAddress : Address + ?1 : Country + ?2 : City (?1) + * ?3 : Street (?1) (?2) +``` +//starts// from the ``Street`` argument, +which enables GF automatically to infer the city and the country. +Thus, in addition to guaranteeing the meaningfulness of the results, +dependent types can shorten editing sessions considerably. + + + +===Dependent types in concrete syntax=== + +The **functional fragment** of GF +terms and types comprises function types, applications, lambda +abstracts, constants, and variables. This fragment is similar in +abstract and concrete syntax. In particular, +dependent types are also available in concrete syntax. +We have not made use of them yet, +but we will now look at one example of how they +can be used. + +Those readers who are familiar with functional programming languages +like ML and Haskell, may already have missed **polymorphic** +functions. For instance, Haskell programmers have access to +the functions +``` + const :: a -> b -> a + const c x = c + + flip :: (a -> b ->c) -> b -> a -> c + flip f y x = f x y +``` +which can be used for any given types ``a``,``b``, and ``c``. + + +The GF counterpart of polymorphic functions are **monomorphic** +functions with explicit **type variables**. Thus the above +definitions can be written +``` + oper const :(a,b : Type) -> a -> b -> a = + \_,_,c,x -> c ; + + oper flip : (a,b,c : Type) -> (a -> b ->c) -> b -> a -> c = + \_,_,_,f,x,y -> f y x ; +``` +When the operations are used, the type checker requires +them to be equipped with all their arguments; this may be a nuisance +for the Haskell or ML programmer. + + + + +===Expressing selectional restrictions=== + +This section introduces a way of using dependent types to +formalize a notion known as **selectional restrictions** +in linguistics. We first present a mathematical model +of the notion, and then integrate it in a linguistically +motivated syntax. + +In linguistics, a +grammar is usually thought of as being about **syntactic well-formedness** +in a rather liberal sense: an expression can be well-formed without +being meaningful, in other words, without being +**semantically well-formed**. +For instance, the sentence +``` + the number 2 is equilateral +``` +is syntactically well-formed but semantically ill-formed. +It is well-formed because it combines a well-formed +noun phrase ("the number 2") with a well-formed +verb phrase ("is equilateral") in accordance with the +rule that the verb phrase is inflected in the +number of the noun phrase: +``` + fun PredV1 : NP -> V1 -> S ; + lin PredV1 np v1 = {s = np.s ++ v1.s ! np.n} ; +``` +It is ill-formed because the predicate "is equilateral" +is only defined for triangles, not for numbers. + + + +In a straightforward type-theoretical formalization of +mathematics, domains of mathematical objects +are defined as types. In GF, we could write +``` + cat Nat ; + cat Triangle ; + cat Prop ; +``` +for the types of natural numbers, triangles, and propositions, +respectively. +Noun phrases are typed as objects of basic types other than +``Prop``, whereas verb phrases are functions from basic types +to ``Prop``. For instance, +``` + fun two : Nat ; + fun Even : Nat -> Prop ; + fun Equilateral : Triangle -> Prop ; +``` +With these judgements, and the linearization rules +``` + lin two = ss ["the number 2"] ; + lin Even x = ss (x.s ++ ["is even"]) ; + lin Equilateral x = ss (x.s ++ ["is equilateral"]) ; +``` +we can form the proposition ``Even two`` +``` + the number 2 is even +``` +but no proposition linearized to +``` + the number 2 is equilateral +``` +since ``Equilateral two`` is not a well-formed type-theoretical object. + + +When formalizing mathematics, e.g. in the purpose of +computer-assisted theorem proving, we are certainly interested +in semantic well-formedness: we want to be sure that a proposition makes +sense before we make the effort of proving it. The straightforward typing +of nouns and predicates shown above is the way in which this +is guaranteed in various proof systems based on type theory. +(Notice that it is still possible to form //false// propositions, +e.g. "the number 3 is even". +False and meaningless are different things.) + + + +As shown by the linearization rules for ``two``, ``Even``, +etc, it //is// possible to use straightforward mathematical typings +as the abstract syntax of a grammar. However, this syntax is not very +expressive linguistically: for instance, there is no distinction between +adjectives and verbs. It is hard to give rules for structures like +adjectival modification ("even number") and conjunction of predicates +("even or odd"). + +By using dependent types, it is simple to combine a linguistically +motivated system of categories with mathematically motivated +type restrictions. What we need is a category of domains of +individual objects, +``` + cat Dom +``` +and dependencies of other categories on this: +``` + cat + S ; -- sentence + V1 Dom ; -- one-place verb + V2 Dom Dom ; -- two-place verb + A1 Dom ; -- one-place adjective + A2 Dom Dom ; -- two-place adjective + PN Dom ; -- proper name + NP Dom ; -- noun phrase + Conj ; -- conjunction + Det ; -- determiner +``` +The number of ``Dom`` arguments depends on the semantic type +corresponding to the category: one-place verbs and adjectives +correspond to types of the form +``` + A -> Prop +``` +whereas two-place verbs and adjectives correspond to types of the form +``` + A -> B -> Prop +``` +where the domains ``A`` and ``B`` can be distinct. +Proper names correspond to types of the form +``` + A +``` +that is, individual objects of the domain ``A``. Noun phrases +correspond to +``` + (A -> Prop) -> Prop +``` +that is, **quantifiers** over the domain ``A``. +Sentences, conjunctions, and determiners correspond to +``` + Prop + Prop -> Prop -> Prop + (A : Dom) -> (A -> Prop) -> Prop +``` +respectively, +and are thus independent of domain. As for common nouns ``CN``, +the simplest semantics is that they correspond to +``` + Dom +``` +In this section, we will, in fact, write ``Dom`` instead of ``CN``. + +Having thus parametrized categories on domains, we have to reformulate +the rules of predication, etc, accordingly. This is straightforward: +``` + fun + PredV1 : (A : Dom) -> NP A -> V1 A -> S ; + ComplV2 : (A,B : Dom) -> V2 A B -> NP B -> V1 A ; + UsePN : (A : Dom) -> PN A -> NP A ; + DetCN : Det -> (A : Dom) -> NP A ; + ModA1 : (A : Dom) -> A1 A -> Dom ; + ConjS : Conj -> S -> S -> S ; + ConjV1 : (A : Dom) -> Conj -> V1 A -> V1 A -> V1 A ; +``` +In linearization rules, +we typically use wildcards for the domain arguments, +to get arities right: +``` + lin + PredV1 _ np vp = ss (np.s ++ vp.s) ; + ComplV2 _ _ v2 np = ss (v2.s ++ np.s) ; + UsePN _ pn = pn ; + DetCN det cn = ss (det.s ++ cn.s) ; + ModA1 cn a1 = ss (a1.s ++ cn.s) ; + ConjS conj s1 s2 = ss (s1.s ++ conj.s ++ s2.s) ; + ConjV1 _ conj v1 v2 = ss (v1.s ++ conj.s ++ v2.s) ; +``` +The domain arguments thus get suppressed in linearization. +Parsing initially returns metavariables for them, +but type checking can usually restore them +by inference from those arguments that are not suppressed. + +One traditional linguistic example of domain restrictions +(= selectional restrictions) is the contrast between the two sentences +``` + John plays golf + golf plays John +``` +To explain the contrast, we introduce the functions +``` + human : Dom ; + game : Dom ; + play : V2 human game ; + John : PN human ; + Golf : PN game ; +``` +Both sentences still pass the context-free parser, +returning trees with lots of metavariables of type ``Dom``: +``` + PredV1 ?0 (UsePN ?1 John) (ComplV2 ?2 ?3 play (UsePN ?4 Golf)) + + PredV1 ?0 (UsePN ?1 Golf) (ComplV2 ?2 ?3 play (UsePN ?4 John)) +``` +But only the former sentence passes the type checker, which moreover +infers the domain arguments: +``` + PredV1 human (UsePN human John) (ComplV2 human game play (UsePN game Golf)) +``` + +A known problem with selectional restrictions is that they can be more +or less liberal. For instance, +``` + John loves Mary + John loves golf +``` +both make sense, even though ``Mary`` and ``golf`` +are of different types. A natural solution in this case is to +formalize ``love`` as a **polymorphic** verb, which takes +a human as its first argument but an object of any type as its second +argument: +``` + fun love : (A : Dom) -> V2 human A ; + lin love _ = ss "loves" ; +``` +Problems remain, such as **subtyping** (e.g. what +is meaningful for a ``human`` is also meaningful for +a ``man`` and a ``woman``, but not the other way round) +and the **extended use** of expressions (e.g. a metaphoric use that +makes sense of "golf plays John"). + + + + + +===Proof objects=== + +Perhaps the most well-known feature of constructive type theory is +the **Curry-Howard isomorphism**, also known as the +**propositions as types principle**. Its earliest formulations +were attempts to give semantics to the logical systems of +propositional and predicate calculus. In this section, we will consider +a more elementary example, showing how the notion of proof is useful +outside mathematics, as well. + +We first define the category of unary (also known as Peano-style) +natural numbers: +``` + cat Nat ; + fun Zero : Nat ; + fun Succ : Nat -> Nat ; +``` +The **successor function** ``Succ`` generates an infinite +sequence of natural numbers, beginning from ``Zero``. + + + +We then define what it means for a number //x// to be less than +a number //y//. Our definition is based on two axioms: +- ``Zero`` is less than ``Succ y`` for any ``y``. +- If ``x`` is less than ``y``, then``Succ x`` is less than ``Succ y``. + + +The most straightforward way of expressing these axioms in type theory +is as typing judgements that introduce objects of a type ``Less x y``: +``` + cat Less Nat Nat ; + fun lessZ : (y : Nat) -> Less Zero (Succ y) ; + fun lessS : (x,y : Nat) -> Less x y -> Less (Succ x) (Succ y) ; +``` +Objects formed by ``lessZ`` and ``lessS`` are +called **proof objects**: they establish the truth of certain +mathematical propositions. +For instance, the fact that 2 is less that +4 has the proof object +``` + lessS (Succ Zero) (Succ (Succ (Succ Zero))) + (lessS Zero (Succ (Succ Zero)) (lessZ (Succ Zero))) +``` +whose type is +``` + Less (Succ (Succ Zero)) (Succ (Succ (Succ (Succ Zero)))) +``` +which is the same thing as the proposition that 2 is less than 4. + + + +GF grammars can be used to provide a **semantic control** of +well-formedness of expressions. We have already seen examples of this: +the grammar of well-formed addresses and the grammar with +selectional restrictions above. By introducing proof objects +we have now added a very powerful +technique of expressing semantic conditions. + + + +A simple example of the use of proof objects is the definition of +well-formed //time spans//: a time span is expected to be from an earlier to +a later time: +``` + from 3 to 8 +``` +is thus well-formed, whereas +``` + from 8 to 3 +``` +is not. The following rules for spans impose this condition +by using the ``Less`` predicate: +``` + cat Span ; + fun span : (m,n : Nat) -> Less m n -> Span ; +``` + + + + +===Variable bindings=== + +Mathematical notation and programming languages have lots of +expressions that **bind** variables. For instance, +a universally quantifier proposition +``` + (All x)B(x) +``` +consists of the **binding** ``(All x)`` of the variable ``x``, +and the **body** ``B(x)``, where the variable ``x`` is +said to occur bound. + +Variable bindings appear in informal mathematical language as well, for +instance, +``` + for all x, x is equal to x + + the function that for any numbers x and y returns the maximum of x+y + and x*y +``` + +In type theory, variable-binding expression forms can be formalized +as functions that take functions as arguments. The universal +quantifier is defined +``` + fun All : (Ind -> Prop) -> Prop +``` +where ``Ind`` is the type of individuals and ``Prop``, +the type of propositions. If we have, for instance, the equality predicate +``` + fun Eq : Ind -> Ind -> Prop +``` +we may form the tree +``` + All (\x -> Eq x x) +``` +which corresponds to the ordinary notation +``` + (All x)(x = x). +``` + + +An abstract syntax where trees have functions as arguments, as in +the two examples above, has turned out to be precisely the right +thing for the semantics and computer implementation of +variable-binding expressions. The advantage lies in the fact that +only one variable-binding expression form is needed, the lambda abstract +``\x -> b``, and all other bindings can be reduced to it. +This makes it easier to implement mathematical theories and reason +about them, since variable binding is tricky to implement and +to reason about. The idea of using functions as arguments of +syntactic constructors is known as **higher-order abstract syntax**. + +The question now arises: how to define linearization rules +for variable-binding expressions? +Let us first consider universal quantification, +``` + fun All : (Ind -> Prop) -> Prop. +``` +We write +``` + lin All B = {s = "(" ++ "All" ++ B.$0 ++ ")" ++ B.s} +``` +to obtain the form shown above. +This linearization rule brings in a new GF concept - the ``v`` +field of ``B`` containing a bound variable symbol. +The general rule is that, if an argument type of a function is +itself a function type ``A -> C``, the linearization type of +this argument is the linearization type of ``C`` +together with a new field ``$0 : Str``. In the linearization rule +for ``All``, the argument ``B`` thus has the linearization +type +``` + {$0 : Str ; s : Str}, +``` +since the linearization type of ``Prop`` is +``` + {s : Str} +``` +(we remind that the order of fields in a record does not matter). +In other words, the linearization of a function +consists of a linearization of the body together with a +field for a linearization of the bound variable. +Those familiar with type theory or lambda calculus +should notice that GF requires trees to be in +**eta-expanded** form in order to be linearizable: +any function of type +``` + A -> C +``` +always has a syntax tree of the form +``` + \x -> c +``` +where ``c : C`` under the assumption ``x : A``. +It is in this form that an expression can be analysed +as having a bound variable and a body. + + +Given the linearization rule +``` + lin Eq a b = {s = "(" ++ a.s ++ "=" ++ b.s ++ ")"} +``` +the linearization of +``` + \x -> Eq x x +``` +is the record +``` + {$0 = "x", s = ["( x = x )"]} +``` +Thus we can compute the linearization of the formula, +``` + All (\x -> Eq x x) --> {s = "[( All x ) ( x = x )]"}. +``` + + +How did we get the //linearization// of the variable ``x`` +into the string ``"x"``? GF grammars have no rules for +this: it is just hard-wired in GF that variable symbols are +linearized into the same strings that represent them in +the print-out of the abstract syntax. + + +To be able to +//parse// variable symbols, however, GF needs to know what +to look for (instead of e.g. trying to parse //any// +string as a variable). What strings are parsed as variable symbols +is defined in the lexical analysis part of GF parsing (see below). + +When //editing// with grammars that have +bound variables, the names of bound variables are +selected automatically, but can be changed at any time by +using an Alpha Conversion command. + +If several variables are bound in the same argument, the +labels are ``$0, $1, $2``, etc. + + + +===Semantic definitions=== +We have seen that, +just like functional programming languages, GF has declarations +of functions, telling what the type of a function is. +But we have not yet shown how to **compute** +these functions: all we can do is provide them with arguments +and linearize the resulting terms. +Since our main interest is the well-formedness of expressions, +this has not yet bothered +us very much. As we will see, however, computation does play a role +even in the well-formedness of expressions when dependent types are +present. + + +GF has a form of judgement for **semantic definitions**, +recognized by the key word ``def``. At its simplest, it is just +the definition of one constant, e.g. +``` + def one = succ zero ; +``` +We can also define a function with arguments, +``` + def Neg A = Impl A Abs ; +``` +which is still a special case of the most general notion of +definition, that of a group of **pattern equations**: +``` + def sum x zero = x ; + def sum x (succ y) = succ (sum x y) ; +``` +To compute a term is, as in functional programming languages, +simply to follow a chain of reductions until no definition +can be applied. For instance, we compute +``` + sum one one --> + sum (succ zero) (succ zero) --> + succ (sum (succ zero) zero) --> + succ (succ zero) +``` + +The ``def`` definitions of a grammar induce a notion of +**definitional equality** among trees: two trees are +definitionally equal if they compute into the same tree. +Thus, trivially, all trees in a chain of computation +(such as the one above) +are definitionally equal to each other. So are the trees +``` + sum zero (succ one) + succ one + sum (sum zero zero) (sum (succ zero) one) +``` +and infinitely many other trees. + + + +A fact that has to be emphasized about ``def`` definitions is that +they are //not// performed as a first step of linearization. +We say that **linearization is intensional**, which means that +the definitional equality of two trees does not imply that +they have the same linearizations. For instance, the seven terms +above all have different linearizations in arithmetic notation: +``` + 1 + 1 + s(0) + s(0) + s(s(0) + 0) + s(s(0)) + 0 + s(0) + s(1) + 0 + 0 + s(0) + 1 +``` +This notion of intensionality is +no more exotic than the intensionality of any **pretty-printing** +function of a programming language (function that shows +the expressions of the language as strings). It is vital for +pretty-printing to be intensional in this sense - if we want, +for instance, to trace a chain of computation by pretty-printing each +intermediate step, what we want to see is a sequence of different +expression, which are definitionally equal. + +What is more exotic is that GF has two ways of referring to the +abstract syntax objects. In the concrete syntax, the reference is intentional. +In the abstract syntax itself, the reference is always extensional, since +**type checking is extensional**. The reason is that, +in the type theory with dependent types, types may depend on terms. +Two types depending on terms that are definitionally equal are +equal types. For instance, +``` + Proof (Od one) + Proof (Od (succ zero)) +``` +are equal types. Hence, any tree that type checks as a proof that +1 is odd also type checks as a proof that the successor of 0 is odd. +(Recall, in this connection, that the +arguments a category depends on never play any role +in the linearization of trees of that category, +nor in the definition of the linearization type.) + +In addition to computation, definitions impose a +**paraphrase** relation on expressions: +two strings are paraphrases if they +are linearizations of trees that are +definitionally equal. +Paraphrases are sometimes interesting for +translation: the **direct translation** +of a string, which is the linearization of the same tree +in the targer language, may be inadequate because it is e.g. +unidiomatic or ambiguous. In such a case, +the translation algorithm may be made to consider +translation by a paraphrase. + + +To stress express the distinction between +**constructors** (=**canonical** functions) +and other functions, GF has a judgement form +``data`` to tell that certain functions are canonical, e.g. +``` + data Nat = succ | zero ; +``` +Unlike in Haskell, but similarly to ALF (where constructor functions +are marked with a flag ``C``), +new constructors can be added to +a type with new ``data`` judgements. The type signatures of constructors +are given separately, in ordinary ``fun`` judgements. %--! |