gf and dependent types
87 views
Skip to first unread message
Hans Leiss
Feb 20, 2015, 2:21:18 PM2/20/15
to gf-...@googlegroups.com
Hello Aarne and Peter, especially,
> For instance, record subtyping à la Cardelli
> http://lucacardelli.name/papers/inheritance.pdf
> would make sense, and is as Peter says already supported for linearizations.
> My dream is to try out records like this in the arguments of dependent
> types, so that one could for instance have
> NP car < NP vehicle
> when
> car < vehicle
> in Cardelli's sense. We have discussed this with Per Martin-Löf and he was
> very much in favour. The records themselves are not dependently typed.
this might be useful, but I'm not sure whether one *always* wants to
lift the subtype relation through the dependent type constructor.
My impression is that dependent types in gf are not first-class
types at all, in the sense that (in the current gf) we have
lintype NP car = lintype NP vehicle,
and actually we are only allowed to define
lintype NP = ...,
i.e. lintype assigns a type to the type constructor NP, not to the
different types (NP car), (NP vehicle) independently; as Peter said:
> - it's difficult to get lintypes to work well with dependent types --
> the current solution is the the lintype simply ignore dependencies,
> which makes dependent tpyes even less useful
I don't really understand why ignoring dependencies should be
necessary. In the grammar I attach, I wanted to implement
lintype (CN count) = { s : Num => Case => Str ; ... }
(CN mass) = { s : Case => Str ; ... }
and exclude plural for mass nouns altogether, which I couldn't in gf.
So, before you can have (NP car) < (NP vehicle), there's something
to do even to get (NP car) =/= (NP vehicle).
Another thing I was puzzled by is that for number-dependent np's
cat Number; NP Number ;
fun sg, pl : Number ;
I couldn't define
param Num = Sg | Pl ;
lincat Number = {n : Num} ;
lin sg = {n : Sg} ;
but was forced to add a Str-field: lincat Number = {s:Str; n:Num}
works. I don't see that the GF-book, C.4.7, demands an s:Str-field.
Remark: Actually I wanted the simpler definition
param Num = Sg | Pl ;
lincat Number = Num ;
lin sg = Sg ; pl = Pl ;
but then I could not use the dependent argument k as in
fun f : (k:Number) -> ...
lin f k x = ... k ... ;
apparently, the k:Number is not turned into a k:Num in the
lin-definition, at least I couldn't store k in a Num-field.
> - after 15 years of GF, almost no grammars make use of dependent types,
> so it's probably not extremely useful in practise
Below, Peter, is a little example grammar that uses dependent types in
syntax to separate NPs into (NP sg), (NP pl) [and artificial, empty (NP
any)] and distinguishes between verbs (and VP,VPSlash) that impose
number restrictions on their arguments. The point is to exclude singular
NPs from positions where a plural is demanded, either by lexical
properties of verbs or by reciprocal constructions.
In some sense, there is a nice, uniform dependency on number going on,
which makes the use of dependent types attractive, but on the other
hand, many verb/VPSlash arguments don't care about number, and there we
would need better subtyping (than the (VP any) as (VP sg) + (VP pl) I am
using, plus some extra grammar rules dealing with number=any).
To complete this exercise, one should add a Montague-semantics showing
that the plural quantifier cannot be reduced to the singular quantifier,
in sentences like
some/these lines don't intersect (each other).
[ * some/this line does not intersect ]
But this would be more work ...
Best,
Hans
> For instance, record subtyping à la Cardelli
> http://lucacardelli.name/papers/inheritance.pdf
> would make sense, and is as Peter says already supported for linearizations.
> My dream is to try out records like this in the arguments of dependent
> types, so that one could for instance have
> NP car < NP vehicle
> when
> car < vehicle
> in Cardelli's sense. We have discussed this with Per Martin-Löf and he was
> very much in favour. The records themselves are not dependently typed.
this might be useful, but I'm not sure whether one *always* wants to
lift the subtype relation through the dependent type constructor.
My impression is that dependent types in gf are not first-class
types at all, in the sense that (in the current gf) we have
lintype NP car = lintype NP vehicle,
and actually we are only allowed to define
lintype NP = ...,
i.e. lintype assigns a type to the type constructor NP, not to the
different types (NP car), (NP vehicle) independently; as Peter said:
> - it's difficult to get lintypes to work well with dependent types --
> the current solution is the the lintype simply ignore dependencies,
> which makes dependent tpyes even less useful
I don't really understand why ignoring dependencies should be
necessary. In the grammar I attach, I wanted to implement
lintype (CN count) = { s : Num => Case => Str ; ... }
(CN mass) = { s : Case => Str ; ... }
and exclude plural for mass nouns altogether, which I couldn't in gf.
So, before you can have (NP car) < (NP vehicle), there's something
to do even to get (NP car) =/= (NP vehicle).
Another thing I was puzzled by is that for number-dependent np's
cat Number; NP Number ;
fun sg, pl : Number ;
I couldn't define
param Num = Sg | Pl ;
lincat Number = {n : Num} ;
lin sg = {n : Sg} ;
but was forced to add a Str-field: lincat Number = {s:Str; n:Num}
works. I don't see that the GF-book, C.4.7, demands an s:Str-field.
Remark: Actually I wanted the simpler definition
param Num = Sg | Pl ;
lincat Number = Num ;
lin sg = Sg ; pl = Pl ;
but then I could not use the dependent argument k as in
fun f : (k:Number) -> ...
lin f k x = ... k ... ;
apparently, the k:Number is not turned into a k:Num in the
lin-definition, at least I couldn't store k in a Num-field.
> - after 15 years of GF, almost no grammars make use of dependent types,
> so it's probably not extremely useful in practise
Below, Peter, is a little example grammar that uses dependent types in
syntax to separate NPs into (NP sg), (NP pl) [and artificial, empty (NP
any)] and distinguishes between verbs (and VP,VPSlash) that impose
number restrictions on their arguments. The point is to exclude singular
NPs from positions where a plural is demanded, either by lexical
properties of verbs or by reciprocal constructions.
In some sense, there is a nice, uniform dependency on number going on,
which makes the use of dependent types attractive, but on the other
hand, many verb/VPSlash arguments don't care about number, and there we
would need better subtyping (than the (VP any) as (VP sg) + (VP pl) I am
using, plus some extra grammar rules dealing with number=any).
To complete this exercise, one should add a Montague-semantics showing
that the plural quantifier cannot be reduced to the singular quantifier,
in sentences like
some/these lines don't intersect (each other).
[ * some/this line does not intersect ]
But this would be more work ...
Best,
Hans
Peter Ljunglöf
Feb 23, 2015, 5:54:11 AM2/23/15
to gf-...@googlegroups.com
Hej Hans, Aarne, et al,
> 20 feb 2015 kl. 20:21 skrev Hans Leiss <le...@cis.uni-muenchen.de>:
>
> Hello Aarne and Peter, especially,
>
>> For instance, record subtyping à la Cardelli
>> http://lucacardelli.name/papers/inheritance.pdf
>> would make sense, and is as Peter says already supported for linearizations.
>> My dream is to try out records like this in the arguments of dependent
>> types, so that one could for instance have
>> NP car < NP vehicle
>> when
>> car < vehicle
>> in Cardelli's sense. We have discussed this with Per Martin-Löf and he was
>> very much in favour. The records themselves are not dependently typed.
Aarne, what do you mean with "records themselves are not dependently typed"?
> (...)
Your example (and the other "practical" examples I've seen) relies on non-recursive dependent types. I.e., all types that are used in dependencies are finite (Number in your example). One big reason for this (I think) is that finite dependencies can be compiled away, so we can still use the efficient PMCFG parsing algorithm.
General dependencies are very interesting - they can be used for donkey sentences and semantics - but they have not been used in any practical grammar. I think one reason is that although MLTT a really nice and simple theory, it's too limited to be useful outside of toy systems. Robin Cooper has been trying to make the MLTT ideas more useful for dialogue and semantics with his TTR (Type Theory with Records), but then he gets something that is really complicated instead.
So my refined statement is: General dependent types are not useful for GF, but limited dependencies can very well be, especially if used together with subtyping. But then I would prefer som nice syntactic sugaring, e.g., by using a record-like notation for the dependencies (which can be very many if we want to write large grammars). Something like this perhaps (assuming two Number dependencies for V2):
V2 < V2{subj=Sg} < V2{subj=Sg;obj=Pl} > V2{obj=Pl} > V2
V2 = V2{subj=_;obj=_}
V2{subj=Sg} = V2{subj=Sg;obj=_}
V2{obj=Pl} = V2{subj=_;obj=Pl}
Next step is to merge all V/V2/... into one V with a subcat dependency.
Naturally, the lintypes should be more liberal than currently in GF: lintype V2 < lintype V2{subj=Sg} < ...
/Peter
_______________________________________________________________________
peter ljunglöf
viceprefekt för grundutbildning
institutionen för data- och informationsteknik
göteborgs universitet och chalmers tekniska högskola
> 20 feb 2015 kl. 20:21 skrev Hans Leiss <le...@cis.uni-muenchen.de>:
>
> Hello Aarne and Peter, especially,
>
>> For instance, record subtyping à la Cardelli
>> http://lucacardelli.name/papers/inheritance.pdf
>> would make sense, and is as Peter says already supported for linearizations.
>> My dream is to try out records like this in the arguments of dependent
>> types, so that one could for instance have
>> NP car < NP vehicle
>> when
>> car < vehicle
>> in Cardelli's sense. We have discussed this with Per Martin-Löf and he was
>> very much in favour. The records themselves are not dependently typed.
> (...)
>
>> - after 15 years of GF, almost no grammars make use of dependent types,
>> so it's probably not extremely useful in practise
>
> Below, Peter, is a little example grammar that uses dependent types in
> syntax to separate NPs into (NP sg), (NP pl) [and artificial, empty (NP
> any)] and distinguishes between verbs (and VP,VPSlash) that impose
> number restrictions on their arguments. The point is to exclude singular
> NPs from positions where a plural is demanded, either by lexical
> properties of verbs or by reciprocal constructions.
Yes, I agree that these things can be very nice, so I have to refine my statement a bit:
>> - after 15 years of GF, almost no grammars make use of dependent types,
>> so it's probably not extremely useful in practise
>
> Below, Peter, is a little example grammar that uses dependent types in
> syntax to separate NPs into (NP sg), (NP pl) [and artificial, empty (NP
> any)] and distinguishes between verbs (and VP,VPSlash) that impose
> number restrictions on their arguments. The point is to exclude singular
> NPs from positions where a plural is demanded, either by lexical
> properties of verbs or by reciprocal constructions.
Your example (and the other "practical" examples I've seen) relies on non-recursive dependent types. I.e., all types that are used in dependencies are finite (Number in your example). One big reason for this (I think) is that finite dependencies can be compiled away, so we can still use the efficient PMCFG parsing algorithm.
General dependencies are very interesting - they can be used for donkey sentences and semantics - but they have not been used in any practical grammar. I think one reason is that although MLTT a really nice and simple theory, it's too limited to be useful outside of toy systems. Robin Cooper has been trying to make the MLTT ideas more useful for dialogue and semantics with his TTR (Type Theory with Records), but then he gets something that is really complicated instead.
So my refined statement is: General dependent types are not useful for GF, but limited dependencies can very well be, especially if used together with subtyping. But then I would prefer som nice syntactic sugaring, e.g., by using a record-like notation for the dependencies (which can be very many if we want to write large grammars). Something like this perhaps (assuming two Number dependencies for V2):
V2 < V2{subj=Sg} < V2{subj=Sg;obj=Pl} > V2{obj=Pl} > V2
V2 = V2{subj=_;obj=_}
V2{subj=Sg} = V2{subj=Sg;obj=_}
V2{obj=Pl} = V2{subj=_;obj=Pl}
Next step is to merge all V/V2/... into one V with a subcat dependency.
Naturally, the lintypes should be more liberal than currently in GF: lintype V2 < lintype V2{subj=Sg} < ...
/Peter
_______________________________________________________________________
peter ljunglöf
viceprefekt för grundutbildning
institutionen för data- och informationsteknik
göteborgs universitet och chalmers tekniska högskola
Aarne Ranta
Feb 23, 2015, 2:13:32 PM2/23/15
to gf-...@googlegroups.com
Peter, Hans, all
On Mon, Feb 23, 2015 at 11:54 AM, Peter Ljunglöf <peter.l...@cse.gu.se> wrote:
Hej Hans, Aarne, et al,
> 20 feb 2015 kl. 20:21 skrev Hans Leiss <le...@cis.uni-muenchen.de>:
>
> Hello Aarne and Peter, especially,
>
>> For instance, record subtyping à la Cardelli
>> http://lucacardelli.name/papers/inheritance.pdf
>> would make sense, and is as Peter says already supported for linearizations.
>> My dream is to try out records like this in the arguments of dependent
>> types, so that one could for instance have
>> NP car < NP vehicle
>> when
>> car < vehicle
>> in Cardelli's sense. We have discussed this with Per Martin-Löf and he was
>> very much in favour. The records themselves are not dependently typed.
Aarne, what do you mean with "records themselves are not dependently typed"?
That they are of the form {x : A ; y : B} rather than {x : A ; y : B(x)}. It is the latter that has been difficult to understand fully, despite of efforts e.g. in the Agda series of frameworks.
> (...)
>
>> - after 15 years of GF, almost no grammars make use of dependent types,
>> so it's probably not extremely useful in practise
>
> Below, Peter, is a little example grammar that uses dependent types in
> syntax to separate NPs into (NP sg), (NP pl) [and artificial, empty (NP
> any)] and distinguishes between verbs (and VP,VPSlash) that impose
> number restrictions on their arguments. The point is to exclude singular
> NPs from positions where a plural is demanded, either by lexical
> properties of verbs or by reciprocal constructions.
Yes, I agree that these things can be very nice, so I have to refine my statement a bit:
Your example (and the other "practical" examples I've seen) relies on non-recursive dependent types. I.e., all types that are used in dependencies are finite (Number in your example). One big reason for this (I think) is that finite dependencies can be compiled away, so we can still use the efficient PMCFG parsing algorithm.
I agree. Finite dt's are still a nice way to factor the code.
General dependencies are very interesting - they can be used for donkey sentences and semantics - but they have not been used in any practical grammar. I think one reason is that although MLTT a really nice and simple theory, it's too limited to be useful outside of toy systems. Robin Cooper has been trying to make the MLTT ideas more useful for dialogue and semantics with his TTR (Type Theory with Records), but then he gets something that is really complicated instead.
Given the success of Coq and Agda in the formalization of mathematics, I don't quite agree with the word "toy".
In GF, one should mention Kristofer Johannisson's GF-KeY plug-in, which was used in a real system,
as well and the implementation of SUMO ontology by Krasimir Angelov and Ramona Enache
Not wide-coverage parsers, but certainly more than toys.
So my refined statement is: General dependent types are not useful for GF, but limited dependencies can very well be,
I don't agree at all. There is so much potential that remains to be used.
especially if used together with subtyping. But then I would prefer som nice syntactic sugaring, e.g., by using a record-like notation for the dependencies (which can be very many if we want to write large grammars). Something like this perhaps (assuming two Number dependencies for V2):
V2 < V2{subj=Sg} < V2{subj=Sg;obj=Pl} > V2{obj=Pl} > V2
V2 = V2{subj=_;obj=_}
V2{subj=Sg} = V2{subj=Sg;obj=_}
V2{obj=Pl} = V2{subj=_;obj=Pl}
Next step is to merge all V/V2/... into one V with a subcat dependency.
This has been done :-) https://www.aclweb.org/anthology/W/W14/W14-1401.pdf
Naturally, the lintypes should be more liberal than currently in GF: lintype V2 < lintype V2{subj=Sg} < ...
A thing one has to keep in mind when making lincat's dependent on type dependencies is that it is a common pattern to write
fun f : (x : A) -> B(x) -> C(x)
The linearization rule must thus be something like
lin f x b = case x of {...}
since the types B(x) and C(x) can be different in different branches of the case expression.
Moreover, even A is an infinite set, I lincat B(x) must generate a finite number of types in order for PMCFG to work.
Regards
Aarne.
/Peter
_______________________________________________________________________
peter ljunglöf
viceprefekt för grundutbildning
institutionen för data- och informationsteknik
göteborgs universitet och chalmers tekniska högskola
--
---
You received this message because you are subscribed to the Google Groups "Grammatical Framework" group.
To unsubscribe from this group and stop receiving emails from it, send an email to gf-dev+un...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Peter Ljunglöf
Feb 23, 2015, 4:06:42 PM2/23/15
to gf-...@googlegroups.com
I tried to be provocative, but didn't succeed that well...
> 23 feb 2015 kl. 20:13 skrev Aarne Ranta <aa...@chalmers.se>:
>
> Peter, Hans, all
>
>> On Mon, Feb 23, 2015 at 11:54 AM, Peter Ljunglöf <peter.l...@cse.gu.se> wrote:
>>
>> (...)
>> General dependencies are very interesting - they can be used for donkey sentences and semantics - but they have not been used in any practical grammar. I think one reason is that although MLTT a really nice and simple theory, it's too limited to be useful outside of toy systems. Robin Cooper has been trying to make the MLTT ideas more useful for dialogue and semantics with his TTR (Type Theory with Records), but then he gets something that is really complicated instead.
>
> Given the success of Coq and Agda in the formalization of mathematics, I don't quite agree with the word "toy".
Hehe... I meant in the context of natural language grammar of course, not logic :)
> In GF, one should mention Kristofer Johannisson's GF-KeY plug-in, which was used in a real system,
>
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.100.2684&rep=rep1&type=pdf
>
> as well and the implementation of SUMO ontology by Krasimir Angelov and Ramona Enache
>
> http://link.springer.com/chapter/10.1007/978-3-642-31175-8_1#page-1
>
> Not wide-coverage parsers, but certainly more than toys.
Ok, I stand (half-)corrected - I didn't know that they used non-finite dependent types.
>> So my refined statement is: General dependent types are not useful for GF, but limited dependencies can very well be,
>
> I don't agree at all. There is so much potential that remains to be used.
Let's hope so. But I personally still feel that subtyping is more useful than dependent types, and I would prefer to restrict the dependencies to finite if that makes it possible to add subtyping.
>> especially if used together with subtyping. But then I would prefer som nice syntactic sugaring, e.g., by using a record-like notation for the dependencies (which can be very many if we want to write large grammars). Something like this perhaps (assuming two Number dependencies for V2):
>>
>> V2 < V2{subj=Sg} < V2{subj=Sg;obj=Pl} > V2{obj=Pl} > V2
>>
>> V2 = V2{subj=_;obj=_}
>> V2{subj=Sg} = V2{subj=Sg;obj=_}
>> V2{obj=Pl} = V2{subj=_;obj=Pl}
>>
>> Next step is to merge all V/V2/... into one V with a subcat dependency.
>
> This has been done :-) https://www.aclweb.org/anthology/W/W14/W14-1401.pdf
Yes I know, that one is nice, and subtyping would make it even nicer :)
>> Naturally, the lintypes should be more liberal than currently in GF: lintype V2 < lintype V2{subj=Sg} < ...
>
> A thing one has to keep in mind when making lincat's dependent on type dependencies is that it is a common pattern to write
>
> fun f : (x : A) -> B(x) -> C(x)
>
> The linearization rule must thus be something like
>
> lin f x b = case x of {...}
>
> since the types B(x) and C(x) can be different in different branches of the case expression.
Yes, that's a problem.
> Moreover, even A is an infinite set, I lincat B(x) must generate a finite number of types in order for PMCFG to work.
Sorry, I didn't get that.
/Peter
> 23 feb 2015 kl. 20:13 skrev Aarne Ranta <aa...@chalmers.se>:
>
> Peter, Hans, all
>
>> On Mon, Feb 23, 2015 at 11:54 AM, Peter Ljunglöf <peter.l...@cse.gu.se> wrote:
>>
>> Aarne, what do you mean with "records themselves are not dependently typed"?
>
> That they are of the form {x : A ; y : B} rather than {x : A ; y : B(x)}. It is the latter that has been difficult to understand fully, despite of efforts e.g. in the Agda series of frameworks.
Yes that is a difficult path.
>
> That they are of the form {x : A ; y : B} rather than {x : A ; y : B(x)}. It is the latter that has been difficult to understand fully, despite of efforts e.g. in the Agda series of frameworks.
>> General dependencies are very interesting - they can be used for donkey sentences and semantics - but they have not been used in any practical grammar. I think one reason is that although MLTT a really nice and simple theory, it's too limited to be useful outside of toy systems. Robin Cooper has been trying to make the MLTT ideas more useful for dialogue and semantics with his TTR (Type Theory with Records), but then he gets something that is really complicated instead.
>
> Given the success of Coq and Agda in the formalization of mathematics, I don't quite agree with the word "toy".
> In GF, one should mention Kristofer Johannisson's GF-KeY plug-in, which was used in a real system,
>
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.100.2684&rep=rep1&type=pdf
>
> as well and the implementation of SUMO ontology by Krasimir Angelov and Ramona Enache
>
> http://link.springer.com/chapter/10.1007/978-3-642-31175-8_1#page-1
>
> Not wide-coverage parsers, but certainly more than toys.
>> So my refined statement is: General dependent types are not useful for GF, but limited dependencies can very well be,
>
> I don't agree at all. There is so much potential that remains to be used.
>> especially if used together with subtyping. But then I would prefer som nice syntactic sugaring, e.g., by using a record-like notation for the dependencies (which can be very many if we want to write large grammars). Something like this perhaps (assuming two Number dependencies for V2):
>>
>> V2 < V2{subj=Sg} < V2{subj=Sg;obj=Pl} > V2{obj=Pl} > V2
>>
>> V2 = V2{subj=_;obj=_}
>> V2{subj=Sg} = V2{subj=Sg;obj=_}
>> V2{obj=Pl} = V2{subj=_;obj=Pl}
>>
>> Next step is to merge all V/V2/... into one V with a subcat dependency.
>
> This has been done :-) https://www.aclweb.org/anthology/W/W14/W14-1401.pdf
>> Naturally, the lintypes should be more liberal than currently in GF: lintype V2 < lintype V2{subj=Sg} < ...
>
> A thing one has to keep in mind when making lincat's dependent on type dependencies is that it is a common pattern to write
>
> fun f : (x : A) -> B(x) -> C(x)
>
> The linearization rule must thus be something like
>
> lin f x b = case x of {...}
>
> since the types B(x) and C(x) can be different in different branches of the case expression.
> Moreover, even A is an infinite set, I lincat B(x) must generate a finite number of types in order for PMCFG to work.
/Peter
Krasimir Angelov
Feb 24, 2015, 3:44:45 AM2/24/15
to Grammatical Framework
An interesting discussion is going on :-). Let me add a few bits that I had in mind for some time.
One problem is that currently the parser completely ignores the dependent types. It parses with the context-free backbone of the abstract syntax and then it does type checking as a post-processing step. This means that for instance the word completion will make suggestions that are irrelevant. Unfortunately this cannot be solved unless if we either:
- restrict ourself to finite dependencies, or
- resort to a parser which uses naive backtracking.
Both options have obvious disadvantages, but they can be partially useful. For example, the compiler could try to detect finite dependencies and then treat them separately. This doesn't have to be a language restriction. It also might be possible to have a parsing algorithm which does backtracking when the abstract syntax has non-finite dependencies and do chart parsing otherwise. The two strategies might also be mixed.
About subtyping:
Subtyping naturally appears with dependent types. Think about this category:
cat A Nat;
i.e. a category indexed with a natural number. We could have rules like:
f : (x : Nat) -> A (succ x) -> S;
g : (x : Nat) -> A x -> S;
Here A (succ x) could be treated as a subtype of A x since only some of the productions for A will produce non-zero index. Currently this information is ignored while parsing although it could be statically determined. Ideally the compiler should detect finite dependencies and compile them into appropriate concrete syntax rules which respect the dependencies. If the dependencies are not finite then it should take into account static subtyping relations such as above.
Subtyping with record types should be just another example. For example B {has_legs=<>; has_wings=<>} should be a subtype of B {has_legs=<>}.
I think the main problem with depend types is that this is underdeveloped feature of the language. This starts from the compiler which fails to type check some dependently typed programs. There are also language features known from Agda and Coq which are missing in GF. They make programming a lot easier and without them dependently typed programs get a bit clumpsy. I myself have experienced this when I tried non-trivial things in GF. I had worked a bit on this but there is a lot more to be done both in the compiler and in the runtime.
The C runtime now has some bits that gets it closer to supporting dependent types. For instance it can compile def rules in the abstract syntax into native code which should run as fast as unoptimized Haskell program. There is a skeleton of a typechecker. The next step is to add unification and to use it in the type checker. A subtyping of the kind for category A is also something that I have planned. Adding record types sounds more difficult is probably possible.
Regards,
Krasimir
Hans Leiss
Feb 24, 2015, 4:52:40 AM2/24/15
to gf-...@googlegroups.com, gf-...@googlegroups.com
Thanks for the discussion!
> >> Aarne, what do you mean with "records themselves are not dependently
> >> typed"?
> >
> > That they are of the form {x : A ; y : B} rather than {x : A ; y :
> > B(x)}. It is the latter that has been difficult to understand fully,
> > despite of efforts e.g. in the Agda series of frameworks.
> Yes that is a difficult path.
I thought you just meant that in {x:A ; y:B}, A and B are simple types.
The type {x : A ; y : B(x)} consists of values {x=a:A ; y=b:B(a)},
right? This looks indeed strange since the record is unordered, so no
component clearly is argument or value domain, and one would immediately
be lead to reciprocal dependencies {x : A(y) ; y : B(x)}. Remotely
reminds me of branching quantifies in logic ...
> >> Next step is to merge all V/V2/... into one V with a subcat dependency.
> >
> > This has been done :-) https://www.aclweb.org/anthology/W/W14/W14-1401.pdf
> Yes I know, that one is nice, and subtyping would make it even nicer :)
Thanks for the link, Aarne. On a first glimpse into the paper, I also
missed the merging of the dependent categories (V x) into a hierarchy.
My feeling is that different syntactic constructions operate on
different domains, but these can overlap in many ways, and indexed
families of disjoint types do not capture this properly. On the other
hand, in a grammar with subtypes, a simple modification to subtype
declarations can change the behaviour in perhaps unexpected ways. But it
seems easier to by and by refine the grammar by adding subtypes at
appropriate places. (If solving subtype constraints were neccessary in
type checking: this problem is NP hard with non-empty record types and
another type constructor, as shown by Vorobyev, even without atomic
types.)
> > Moreover, even A is an infinite set, I lincat B(x) must generate a
> > finite number of types in order for PMCFG to work.
> Sorry, I didn't get that.
You mean because the types correspond to the finitely many nonterminals
of the PMCFG, I assume. But what then is a typical example for a grammar
rule f where A in
> fun f : (x : A) -> B(x) -> C(x)
is infinite?
Best,
Hans
> >> Aarne, what do you mean with "records themselves are not dependently
> >> typed"?
> >
> > That they are of the form {x : A ; y : B} rather than {x : A ; y :
> > B(x)}. It is the latter that has been difficult to understand fully,
> > despite of efforts e.g. in the Agda series of frameworks.
> Yes that is a difficult path.
The type {x : A ; y : B(x)} consists of values {x=a:A ; y=b:B(a)},
right? This looks indeed strange since the record is unordered, so no
component clearly is argument or value domain, and one would immediately
be lead to reciprocal dependencies {x : A(y) ; y : B(x)}. Remotely
reminds me of branching quantifies in logic ...
> >> Next step is to merge all V/V2/... into one V with a subcat dependency.
> >
> > This has been done :-) https://www.aclweb.org/anthology/W/W14/W14-1401.pdf
> Yes I know, that one is nice, and subtyping would make it even nicer :)
missed the merging of the dependent categories (V x) into a hierarchy.
My feeling is that different syntactic constructions operate on
different domains, but these can overlap in many ways, and indexed
families of disjoint types do not capture this properly. On the other
hand, in a grammar with subtypes, a simple modification to subtype
declarations can change the behaviour in perhaps unexpected ways. But it
seems easier to by and by refine the grammar by adding subtypes at
appropriate places. (If solving subtype constraints were neccessary in
type checking: this problem is NP hard with non-empty record types and
another type constructor, as shown by Vorobyev, even without atomic
types.)
> > Moreover, even A is an infinite set, I lincat B(x) must generate a
> > finite number of types in order for PMCFG to work.
> Sorry, I didn't get that.
of the PMCFG, I assume. But what then is a typical example for a grammar
rule f where A in
> fun f : (x : A) -> B(x) -> C(x)
Best,
Hans
Reply all
Reply to author
Forward
0 new messages