Indexed type vs type of functional sort

[Yannick Duchêne]

Hi there,

Formally speaking, does it make any difference to talk about an indexed type and about a type of a functional sort (returning something of any type sort).

I would say it’s the same, but I prefer to ask.

[Steinway Wu]

I think they are the same. Indexed type is a static term of sort "type". A type of a functional sort is just a type constructor of sort "a -> type". It is not yet a type per se. But if you apply it on suitable static arguments, it returns a static term of sort "type". 

[Yannick Duchêne]

Le vendredi 29 juin 2018 00:06:36 UTC+2, Steinway Wu a écrit :

I think they are the same. Indexed type is a static term of sort "type". A type of a functional sort is just a type constructor of sort "a -> type". It is not yet a type per se. But if you apply it on suitable static arguments, it returns a static term of sort "type". 

I agree.

Talking about type constructor, I never really care before, but it’s “funny”  the application may be partial. You can have a type with free variables.

Say you have this indexed type:

        datatype T(i:int) = C1 | C2 of int(i)

        val a = C1

        val b = C2(1)

        val _ = $showtype(a)

        val _ = $showtype(b)

With `a`, the type is `T(i)` where `i` is left a free static variable. The function is only partially evaluated.

With `b`, the type is `T(1)` where there is no more free variable. The function is fully evaluated.

But may be it’s not OK to say with `a` `i` is free in `T`, since `i` is quantified.

I guess the type of `a` could be said a pattern. Is it OK to say so?

I wonder if there is a specific wording to distinguish between the first case and the second case. Unconstrained and fully constrained?

[Hongwei Xi]

Sometimes, there be a subtlety with the use index types.

Say you have f of the sort int -> type and g of the sort type -> type.

f is an indexed type constructor and g is a polymorphic type constructor.

The sort 'int' is predicative and the sort 'type' is impredicative.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/294289e9-9d7c-474d-ae16-054732b07b42%40googlegroups.com.

[Hongwei Xi]

C1 is of the type {i:int}() -> T(i).

If you write C1, the system pick an existential type variable X for you.

This is what the type of 'a' is T(X) for some X. You can pick your own by

writing C1{i}() for integer i.

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9fefab00-e295-433e-9494-3bdf5011c618%40googlegroups.com.

[Yannick Duchêne]

Le vendredi 29 juin 2018 01:22:40 UTC+2, gmhwxi a écrit :

Sometimes, there be a subtlety with the use index types.

Say you have f of the sort int -> type and g of the sort type -> type.

f is an indexed type constructor and g is a polymorphic type constructor.

The sort 'int' is predicative and the sort 'type' is impredicative.

If I read correctly, `prop -> type`  would be polymorphic too? What about `(int, type) -> type`?

Is this stated by some axiom or is this a consequence of something?

If the wording is not the same, this must mean the logic or the properties is not the same.

(im)predicativity is definitively something important. Unfortunately, I still have issue with it. I tried to relate the question “predicative vs impredicative” to the question “predicate vs proposition”, but it did not help. I have read somewhere the difference between a predicate and a proposition, is this: in a predicate, all variables are free, while in a proposition, all variable are bound to a quantifier. If I’m not wrong, indexed types are impredicative, and their indexes are quantified and also the prop sort is said to be impredicative in ATS2, although I can’t see quantified variables there. It seems close enough so far. But with the sort int which is predicative, I can’t see where there would be free variables. Another way,I tried to understand it after definitions saying is impredicative what is defined with references to generalised properties of itself. But I can’t see how it would apply to sorts like type, prop and others.

[Yannick Duchêne]

Le vendredi 29 juin 2018 01:25:12 UTC+2, gmhwxi a écrit :

C1 is of the type {i:int}() -> T(i).

If you write C1, the system pick an existential type variable X for you.

This is what the type of 'a' is T(X) for some X. You can pick your own by

writing C1{i}() for integer i.

Yes, I was to naive when I wrote this. The variable is obviously not the same, it’s another variable, one different variable is created for each application of the type constructor.  Thanks for the tip about `C1{i}()`.

[Yannick Duchêne]

Le vendredi 29 juin 2018 00:45:51 UTC+2, Yannick Duchêne a écrit :

[…]

Talking about type constructor, I never really care before, but it’s “funny”  the application may be partial. You can have a type with free variables.

[…]

Forget about it, it’s only now I realize static expressions are not computed, they just are. Ex. `2 + 2` is not `4`,

it’s just `2 + 2`; it may only possibly become `4` for a constraint solver.