Though attributes support Type Refinement, Effects, Dependent Types, Substructural Types

[sirinath]

Introduce an attribute system which can be used as an extension point for the type system.

Ref: http://www.ats-lang.org/ http://www.idris-lang.org/ https://www.fstar-lang.org/

[andymcn]

Closing this issue because it's far too vague.

Saying "can we have feature x like language y does it" and giving a link to the main page for language y really isn't very helpful. We aren't familiar with the details of all existing languages and we aren't going to read through the entire docs for a given language without some details.

When opening a request please:

• Be specific about what you're asking for.
• Explain in detail what you want. Giving links with extra information for complex concepts is helpful, but you still need to explain it.
• Give some code examples of what you'd like to be able to do in Pony. Making up rubbish syntax for the purposes of explanation is fine.
• If possible explain how what you're asking for differs from existing Pony features or why you can't do it in Pony already.

[sirinath]

This is type system improvements. E.g.

var i: U32 {Range(20, 100)} = 23

var i: MyObj {SingleReferenced, BorrowChecked} = MyObj.create()

var seed: U32 {Units("m / s")} = 10 k * m / h

[andymcn]

Great, you've given some sample syntax, but you still haven't explained the actual concept.

You're clearly wanting to attach attributes to types, but why? What do they do?

Are these attributes putting proper restrictions on the type or are they just something that can queried voluntarily via some reflection API?

Is your Range something predefined in the language / standard library or something that programmers have to / get to define themselves?

What happens if you try to assign a value outside that range? Is that a compile time error and if so how is it spotted? Should it be a runtime error? In either case, does the 23 have to be a literal, or a compile time constant or just any runtime value?

Is the range part of the actual type of your first i, or only used for that initialisation? If I later try to assign 101 without specifying attributes is that an error?

Similarly is your SingleReferenced something builtin? If so how does it differ from Pony's iso? If it's programmer defined then what things is it allowed to do?

Please explain what you're asking for.

[sirinath]

Range can be predefined in the standard libraries but the programmers should be able to define them also. If it is outside the rage it will be a compile time error but based on the definition of if it is compile time resolution or runtime resolution or at any of the other stages (if can consider staying). SingleReferenced is just as a example substructural type system constraints. This can be defined in the standard library or user defined. The standard library should have common usages defined in them. Also I don't think iso should be baked into the language, but should be defined in a library and we should be able to define our own and perhaps change and extend what is already there. Perhaps this is how it is but I am still new to Pony.

[andymcn]

iso is indeed baked into the language and it has to be. It is part of the reference capability system, which is fundamental to the core of Pony and there is no way the programmer could extend this.

If I've understood you correctly about your SingleReferenced then you can already do this in Pony with an interface and an intersection type.

In general you can only track very few values at compile time, since mostly people don't write programs which only use constants. You can improve things somewhat with approaches like min/max analysis, but you're still very limited. Having something that may be checked at compile time if the compiler can manage it, but otherwise will be checked at runtime and may fail, is a really bad idea. It leads to programmer confusion (which then leads to bugs) and violates several on Pony's core principles.

I'm afraid it very much sounds like you don't know anything like enough about how Pony currently works to be suggesting such big changes.

[sirinath]

Actually this eliminated bugs. Language like SPARK Ada use this to ensure that if a program compiles this meets the spec. This is called Correct by Construction. I showed SingleReferenced as means of an example. This can be very well defined as something else.

var i: MyObj {Referenced(Count(min = 0, max = 10), Used(min = 1)), BorrowChecked} = MyObj.create()

Here there are 0 to 10 references to this object and any referenced object needs to be used at least once.

[andymcn]

Checking that the number of references to a given object stays within a given range requires a huge overhead at runtime to process a reference count guarded by a lock on every object. Pony's reference capability system exists specifically to do this analysis at compile time with 0 runtime cost.

Please investigate Pony in far more depth before suggesting any more huge changes.

[sirinath]

There will be some overhead but there are many languages this does this at an acceptable overhead at compile and runtime. E.g. SPARK Ada is heavily used military, medical, aviation and space applications.

Only change to Pony is support type system extensions through annotation like mechanism and incase if it proof like you should be able to send the proof to be check to a proof assistant. There is Z3 also Leanprover which might be more lean.

[sirinath]

There are even 3rd party Java projects which does this in Java which has a simpler type system. E.g. https://github.com/nhatminhle/cofoja, http://www.key-project.org/. I fail to see how there can be any unacceptable overhead.

[andymcn]

Java already has a massive overhead that we do not consider acceptable for Pony, simply because it runs on a VM and has a stop-the-world garbage collector.

Let me say again, the core of Pony was specifically designed to provide compile time enforcement of single reference, immutability, etc with no runtime overhead. This was done to tackle the exact same bugs you mention for languages like SPARK Ada. So why would we also put in a system that does have a huge runtime overhead, just to make the language feel more like what you are used to?

Allow me to be clear: We really appreciate real user feedback and input. However we will not be adding anything like what you suggest here unless you, or anyone else, provides us with a very good use case that isn't easy to do in existing Pony.

[sirinath]

All the verification is static, i.e., compile time and not too much of a compiler overhead! This is use to prove that the code meets the specification. There is no runtime overhead. Testing is limited to the test case. Here the program is proved to be correct. There are tools to verify Java program also. There is no link between verifying a program and the GC overhead. Verification, i.e., proof of correctness is at compile time.