Re: [GF] variable types for arguments?

[Hans Leiss]

Hello Simon,

> In fact, I want Animal and Human be "subtypes" of LivingForm.
> I browsed the ressource manual, tested some implementations, and coudn't
> figure out how to do that.

> Could you please give me a hand up?
> I want to build some hierachy in my types for clarity reason, is it the way?

On the level of abstract syntax, there is no notion of subtype in GF (as
far as I know). But you can use dependent types and coercion
functions. In your case, this would amount to something like

cat Animate ;
LivingForm Animate ; -- LivingForms depending on values of cat Animate
Sentence ;
fun anim, hum : Animate ;
Jean, Marie : LivingForm hum ; -- i.e. Human := LivingForm hum
Snoopy : LivingForm anim ;
F : (k:Animate) -> LivingForm k -> Sentence ;

but your sentences need the "subtype" as argument, (F hum Jean), (F anim
Snoopy). However, the linearization function for F would ignore the
Animate argument, so you have to define it like

lin F _ y = ... y ... ;

Mimicking subtyping this way seems to get clumsy very quickly (i.e. when
the subtype hierarchy isn't flat).

See also my remark on dependent types in syntax on the GF user group,
posted Jan 26. And of course, when we use coercion functions, we can do
so without using dependent types as well (at the price of more coercion
functions, if I see right).

I am missing subtypes on the abstract level mainly because I would like
to reduce overgeneration by restricting syntax rules (as constructor
functions which are total on their domain) to suitable subcategories.

Hans

[Krasimir Angelov]

2015-02-17 17:27 GMT+01:00 Hans Leiss <le...@cis.uni-muenchen.de>:

I am missing subtypes on the abstract level mainly because I would like
to reduce overgeneration by restricting syntax rules (as constructor
functions which are total on their domain) to suitable subcategories.

 I am missing subtypes as well. They would be very natural thing for all grammars that incorporate some kind of taxonomy. Unfortunately there are both theoretical (how to do type checking in presense of subtypes) and practical (substantial redevelopment) problems in this. As far as I know there is no dependently typed language that supports subtyping. On the other hand there are languages which extend the Hindley-Milner type system with subtypes. It looks like at the current state one should either choose subtypes or dependent types. There aren't theoretical reasons to believe that the two cannot coexist but no one have figured out all intricate details.

For the time being there is one more unsatisfactory solution in GF:

Jean : Human
Marie : Human
Snoopy : Animal

Human_LivingForm : Human -> LivingForm;

Animal_LivingForm : Animal -> LivingForm;

F : LivingForm -> Sentence;

[Peter Ljunglöf]

> 18 feb 2015 kl. 09:02 skrev Krasimir Angelov <kr.an...@gmail.com>:
>
>> 2015-02-17 17:27 GMT+01:00 Hans Leiss <le...@cis.uni-muenchen.de>:
>> I am missing subtypes on the abstract level mainly because I would like
>> to reduce overgeneration by restricting syntax rules (as constructor
>> functions which are total on their domain) to suitable subcategories.
>
> I am missing subtypes as well. They would be very natural thing for all grammars that incorporate some kind of taxonomy. Unfortunately there are both theoretical (how to do type checking in presense of subtypes) and practical (substantial redevelopment) problems in this. As far as I know there is no dependently typed language that supports subtyping. On the other hand there are languages which extend the Hindley-Milner type system with subtypes. It looks like at the current state one should either choose subtypes or dependent types. There aren't theoretical reasons to believe that the two cannot coexist but no one have figured out all intricate details.

Personally I would prefer subtypes to dependent types:

- after 15 years of GF, almost no grammars make use of dependent types, so it's probably not extremely useful in practise
- 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
- on the other hand, subtyping works fine with lintypes -- if A≤B, then we can have lintype(A)≤lintype(B)
- parsing with dependent types is very difficult, except for some special cases (when the dependencies are non-recursive)
- and the special case of non-recursive dependencies is compatible with a subtyping system

Something to look into perhaps?

/Peter

[Krasimir Angelov]

На 18.02.2015 г. 9:55 "Peter Ljunglöf" <peter.l...@heatherleaf.se> написа:
> Personally I would prefer subtypes to dependent types:
>
> - after 15 years of GF, almost no grammars make use of dependent types, so it's probably not extremely useful in practise

I agree but this is a major backwards incompatibility.

[John J. Camilleri]

Interesting point Peter.

The C runtime still doesn't support dependent types, does it? So in some sense, this break with compatibility has already started.

--

---
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.

[Krasimir Angelov]

На 18.02.2015 г. 10:05 "John J. Camilleri" <jo...@johnjcamilleri.com> написа:
>
> Interesting point Peter.
> The C runtime still doesn't support dependent types, does it? So in some sense, this break with compatibility has already started.

Not really. They are just not implemented yet because I don't need them for the translator. This is also why the Haskell runtime is still used for the GF shell.

[Aarne Ranta]

Of course we cannot drop dependent types.

But it could make sense to add subtyping for non-dependent types. Maybe even to a subclass of dependent types where they are well understood. The compiler could just reject illicit uses.

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. 

Interestingly, following the semantics of the categories, NP's are covariant whereas VP's are contravariant, since the vehicle/car appears on the left of an arrow (VP car = car -> Prop)

  VP vehicle < VP car

whereas NP car = (car -> Prop) -> Prop.

Who wants to try?

  Aarne.

--

[Krasimir Angelov]

2015-02-18 10:26 GMT+01:00 Aarne Ranta <aa...@chalmers.se>:

Who wants to try?

Sounds like a PhD topic :-). Or at least majour part of it. Add one-two applications and the thesis is done.

[Simon]

Thank you, especially to Hans and Kr.angelov, the second method meets my needs for now.

Best regards,
Simon