Is the word "sort" overloaded as used in ATS?

[spearman]

I have some confusion still about the word "sort" and how it is used in ATS.

on the one hand, in the sense of PTS a sort (as I understand it) is a 
syntactic category, so instead of just terms and types, a program can now 
have more "orthogonal" syntax structure, e.g. proofs

on the other hand, when sorts are said to be the "types" of static terms, I 
am reminded of "kinds" in Haskell, e.g. the kind of the list constructor [] 
is * -> *, and usually these kind of types are thought of as being "higher" 
kinds.

Haskell now has other base kinds than * (such as Constraint), althought I 
haven't used Haskell much lately, this sounds kind of like a "multi-sorted" 
type system as in PTS.

at some point isn't there some kind of cumulative "sort hierarchy" where 
you have Sort0 \subset Sort1 \subset Sort2 ... or is that treating sorts in 
the wrong way?

however this "higher-kind" construction seems to conflict with the idea 
that sorts are "underlying" to language terms. a quote from this article 
that was recently linked also has got me thinking along these lines: 
http://www.haskellforall.com/2012/06/gadts.html

Thus, it perhaps is more appropriate to think of type-level programming as 
> not being a step "above" value level programming in some sort of heirarchy 
> (i.e. values → types → kinds → hyper-kinds) but rather simply existing on 
> the same plane with different rules. This would imply Haskell programming 
> is simply a hybrid approach of programming using two arenas (the 
> value-level arena where initial objects don't exist and the type-level 
> arena where they do exist). Instead of value-level and type-level 
> programming being two different "levels" (which implies an ordering or 
> hierarchy), maybe they are simply two unordered arenas of programming.
>

i think this is a helpful view to take as sometimes you want to give up 
some type inference so that you can gain more program inference.

as a summary, here is currently how I see ATS from what I have read of the 
documentation and discussions:

https://spearman.github.io/

in light of the above, considering as a concrete example the sort `type`, 
can it be both:

1. the type (sort?) of dynamic terms
2. the sort of nullary type constructors

any thoughts or comments on this are appreciated

-- 
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+unsubscr...@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/fc1f771d-e5be-4501-a680-5b8e9e66b477%40googlegroups.com.

Re: Is the word "sort" overloaded as used in ATS?

[Kiwamu Okabe]

On Tue, Mar 21, 2017 at 6:02 PM, spearman  wrote:
> https://spearman.github.io/

Your page is so great work for me!
I think I found it at the start point learning ATS language!
-- 
Kiwamu Okabe at METASEPI DESIGN

-- 
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+unsubscr...@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/CAEvX6dnw1C1OP_i443ZEcyV%2BqD%2BuZ6JQQjyr2WrU0H5Jj26VgA%40mail.gmail.com.

Re: (Co)monads in ATS

[Hongwei Xi]

No. This has to be done in an unsafe manner as the linear view part is
discarded.


On Tue, Mar 21, 2017 at 9:28 AM, August Alm  wrote:

> Is there a standard way to get the underlying [VT?!] part of a term [x:
> VT]?, i.e., some (polymorphic) function
>
>   VT -> VT?!
>
> or
>
>   ( >> VT?!) -> void
>
> ?
>
> Den söndag 19 mars 2017 kl. 03:16:07 UTC+1 skrev gmhwxi:
>>
>>
>> Is the existence of V merely existence or can it always be written
>>> down constructively in the ATS syntax?
>>>
>>
>> It is merely existence.
>>
>> What I should have written is this:
>>
>> Semantically, a linear value vt can be thought of as a pair (v | t), where
>> v is a linear proof (of some view) and t is some data (non-linear value).
>>
>> Of course, this is all intuition. It would require a huge effort to
>> actually build
>> a model for only the core of ATS.
>>
>>
>> On Saturday, March 18, 2017 at 9:00:33 PM UTC-4, August Alm wrote:
>>>
>>> I know T in VT = (V | T) can be gotten by the syntax VT?!. Is there an
>>> analogous syntax for extracting the view V
>>> from VT ?
>>> Also, I am unsure about how to think about this fact that all viewtypes
>>> are a product of a view and a type,
>>> or more specifically, how it interacts with dependent types. How does it
>>> work in a simple case like
>>>
>>>   VT = [l: agz] (a@l | ptr(l))  ?
>>>
>>> Clearly, VT is not ([l1: agz] a@l1 | [l2: agz] ptr(l2)). Is the
>>> existence of V merely existence or can it always be written
>>> down constructively in the ATS syntax?
>>>
>>>
>>> Den lördag 18 mars 2017 kl. 13:27:07 UTC+1 skrev gmhwxi:

 I really like the notes, too.

 I would like to provide a bit of semantic background on viewtypes.

 As the name suggests, a viewtype is just a view plus a type:

 Semantically, one can always assume the following meta-property:

 Given a viewtype VT, there exists a view V and a type T such that

 VT = (V | T)


 *The linearity of a viewtype entirely comes from the linearity of the
 viewinside it.*

 On Thursday, March 16, 2017 at 11:20:54 AM UTC-4, August Alm wrote:
>
> Hi all!
>
> I just wrote down some sketchy thoughts on monads and comonads in ATS.
> ATS has a very unique type system, so there are (co)monads in ATS that
> simply do not exist in other languages. I'm wondering if this might be
> useful. See the attached and let me know if you have ideas.
>
> Best wishes,
> August
>

>>> Den lördag 18 mars 2017 kl. 13:27:07 UTC+1 skrev gmhwxi:

 I really like the notes, too.

 I would like to provide a bit of semantic background on viewtypes.

 As the name suggests, a viewtype is just a view plus a type:

 Semantically, one can always assume the following meta-property:

 Given a viewtype VT, there exists a view V and a type T such that

 VT = (V | T)


 *The linearity of a viewtype entirely comes from the linearity of the
 viewinside it.*

 On Thursday, March 16, 2017 at 11:20:54 AM UTC-4, August Alm wrote:
>
> Hi all!
>
> I just wrote down some sketchy thoughts on monads and comonads in ATS.
> ATS has a very unique type system, so there are (co)monads in ATS that
> simply do not exist in other languages. I'm wondering if this might be
> useful. See the attached and let me know if you have ideas.
>
> Best wishes,
> August
>

>>> Den lördag 18 mars 2017 kl. 13:27:07 UTC+1 skrev gmhwxi:

 I really like the notes, too.

 I would like to provide a bit of semantic background on viewtypes.

 As the name suggests, a viewtype is just a view plus a type:

 Semantically, one can always assume the following meta-property:

 Given a viewtype VT, there exists a view V and a type T such that

 VT = (V | T)


 *The linearity of a viewtype entirely comes from the linearity of the
 viewinside it.*

 On Thursday, March 16, 2017 at 11:20:54 AM UTC-4, August Alm wrote:
>
> Hi all!
>
> I just wrote down some sketchy thoughts on monads and comonads in ATS.
> ATS has a very unique type system, so there are (co)monads in ATS that
> simply do not exist in other languages. I'm wondering if this might be
> useful. See the attached and let me know if you have ideas.
>
> Best wishes,
> August
>
 --
> 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+unsubscr...@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/3cd0053d-e518-421e-9af1-c32c57240856%
> 

Re: Is the word "sort" overloaded as used in ATS?

[spearman]

It is new just created for this post :) I have only been learning ATS for 
one month

On Tuesday, March 21, 2017 at 2:06:53 AM UTC-7, Kiwamu Okabe wrote:
>
> On Tue, Mar 21, 2017 at 6:02 PM, spearman  > wrote: 
> > https://spearman.github.io/ 
>
> Your page is so great work for me! 
> I think I found it at the start point learning ATS language! 
> -- 
> Kiwamu Okabe at METASEPI DESIGN 
>

-- 
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+unsubscr...@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/7a9bf5a7-0a2b-410a-80ea-ebbed30f30b1%40googlegroups.com.