Effectless ffi

[Dambaev Alexander]

We can define external call as effectless (as I understand, this means "pure" in terns of ATS2);

extern fn sqrt( double) :<> double = "ext#"
extern fn launch_missles( double) :<> double = "ext#"

I do understand, that this is due to goal to make transition from C to ATS to be less painful, but maybe, there should be some flag (like -XSafe for ghc, or maybe -Wall -Werror), which will treat effectless ffi calls to be compile time errors?

And one more generic question: I haven't got if user can introduce new custom effects or are they just a predefined set of effects? Are there any docs about such topics in ATS?

[Artyom Shalkhakov]

Hi Alexander,

пн, 6 мая 2019 г. в 07:16, Dambaev Alexander <ice.r...@gmail.com>:

We can define external call as effectless (as I understand, this means "pure" in terns of ATS2);

extern fn sqrt( double) :<> double = "ext#"
extern fn launch_missles( double) :<> double = "ext#"

I do understand, that this is due to goal to make transition from C to ATS to be less painful, but maybe, there should be some flag (like -XSafe for ghc, or maybe -Wall -Werror), which will treat effectless ffi calls to be compile time errors?

Effect annotations are used in ATS for a different reason (compared to Haskell). Please see HX explaining it here:

https://groups.google.com/d/msg/ats-lang-users/L38Bzie5lsE/OnI1BXq8HoIJ

 

And one more generic question: I haven't got if user can introduce new custom effects or are they just a predefined set of effects? Are there any docs about such topics in ATS?

We have some docs in the wiki, please see:

https://github.com/githwxi/ATS-Postiats/wiki/effects

--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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/c440ad8c-9322-44ca-ba6e-c3aaeabe0ece%40googlegroups.com.

--

Cheers,
Artyom Shalkhakov

[Richard]

I do understand, that this is due to goal to make transition from C to ATS to be less painful, but maybe, there should be some flag (like -XSafe for ghc, or maybe -Wall -Werror), which will treat effectless ffi calls to be compile time errors?

Annotating a function definition with effects can be seen as a programmer-centric way to provide the typechecker with extra information about a functions apparent purity, most often seen in combination with proof functions. Also, effects-tracking is most useful when the characteristic behavior of a function is known to the programmer.

And one more generic question: I haven't got if user can introduce new custom effects or are they just a predefined set of effects? Are there any docs about such topics in ATS?

Only builtin effects are currently supported. Here is some information on the builtin effects, https://github.com/githwxi/ATS-Postiats/wiki/effects

 

[Richard]

Oops, did not see you responded Artyom!

[artyom.s...@gmail.com]

On Monday, May 6, 2019 at 10:21:40 AM UTC+3, Richard wrote:

Oops, did not see you responded Artyom!

Richard you're very welcome to put your own suggestions! Better to reiterate twice than none at all. :-)

[Brandon Barker]

Hi Guys,  Thanks for the discussion.

As usual I don't fully understand or recall some of the relevant issues.

In the online editor I quickly tried out this:

fun double (n: int) :<1> int = n + n

val () = println! ("double(5) = ", double(5))

Which works. But changing :<1> to :<0> fails to compile; i also tried a non-polymorphic identity function for ints and had the same result. So what does :<0> really mean?

I think if we had (1), a way to keep track of purity, i.e., any expressions returning unit must be equivalent to the expression () (hopefully this isn't hard to check..), and (2), a way to tell the compiler to assume that ":" assumes :<0> by default, then we might just get purity checking done for free.

[Richard]

#include "share/atspre_staload.hats"

implement main0() = ()

// If I am not mistaken, all functions in ats have all effects (i.e. :<1>) by default.
// note, :<0> is equivalent to :<>

// Just some thoughts....

fun terminating .<>. (n: int):<> int = n * n

//

// Here we require to provide proof that the function terminates

// so, we just insist that it does (.<>.)

//

// Well it does not seem to be a very effectful function so sure

// though, what is the significance of purity in this case?

//

// Effects tracking in ats is not exactly a contract

// For example,

val terminate = terminating(0xb505)

//

// This typechecks fine however, do you notice something strange about the resulting value?

// Passing a value larger than the square root of INTMAX causes arithmetic overflow...

//

// In this case, what good is a function annotated as pure if it can produce arithmetic overflow?

//

// Let us look at a different example, lets use dependent types to flush out this potential bug...

//

stadef IMAX = 2147483647

fun dependent {n:int | n*n <= IMAX} (n: int(n)): int(n*n) = n*n

// 'depend' below fails typechecking,

// unsolved constraint:

// (46341 * 46341) <= IMAX

val depend = dependent(0xb505)

// however this typechecks,

val depend = dependent(0xb504)

On Wednesday, May 29, 2019 at 1:14:19 PM UTC-4, Brandon Barker wrote:

Hi Guys,  Thanks for the discussion.

As usual I don't fully understand or recall some of the relevant issues.

In the online editor I quickly tried out this:

fun double (n: int) :<1> int = n + n

val () = println! ("double(5) = ", double(5))

Which works. But changing :<1> to :<0> fails to compile; i also tried a non-polymorphic identity function for ints and had the same result. So what does :<0> really mean?

I think if we had (1), a way to keep track of purity, i.e., any expressions returning unit must be equivalent to the expression () (hopefully this isn't hard to check..), and (2), a way to tell the compiler to assume that ":" assumes :<0> by default, then we might just get purity checking done for free.

I think that requiring all functions to be pure in the current implementation of ats2 would produce an environment that would greatly decrease programming productivity :)

 

[Brandon Barker]

Hi Richard - thanks for the instructive examples; I clarified a related point on the wiki. 

I agree, that in its current definition, "pure" is actually stronger than what I had in mind. I think letting the programmer choose the default effect type of functions could be useful when executing a build (though it would also have to take this into account, ideally, when linking with other ATS libraries).  

I was going to see if I could get what I wanted, starting by doing this, and playing around with eliminating effects that don't jive with my notion of "sort of pure" ;-):

implement
main0 () = {

 val () = println! ("double(5) = ", double(5))
}

fun double .<>. (n: int) :<0> int = (
  // print 'h';
  n + n
)

 Unfortunately, this resulted in an error that I don't have time to dive into tonight (was using version 0.3.11 out of convenience). Online, it works (see attached image). However, if I uncomment the print 'h' line, it fails, but i can't see the error online.

[Richard]

When un-commenting 

// print 'h';  

the typechecker issues a warning stating that 

some disallowed effects may be incurred: 1

This is expected behavior as the function signature states that it is pure (:<0>)

To further illustrate the difficulty in relying on effects, one can just as easily silence the compiler with one of the "ats-swiss-army-knives",

fun double .<>. (n: int):<> int =

(

  $effmask{1}(print 'h');

  n + n

)

Here, we just tell the compiler "look, just ignore this one" :)

[Brandon Barker]

OK, cool, I'm not sure which of the listed effects it is catching on, but we can all agree it isn't pure!

I think this could still be useful. Using effmask like this seems a bit like using unsafePerformIO in Haskell; not great, and the one time I've seen it used in a library, it has bitten me - since the library author violated one of the safety tenants - but supposedly there are some good uses for it ;-).

In the end it is hard to get this perfect (you'd need some really nice static analysis tools to check what you're linking in from C-land or other FFIs I imagine), but maybe we can work towards safer code in this way without undue burden on the programmer. 

[Brandon Barker]

Actually maybe it isn't necessary to have compiler flags - it should be reasonable, *I think*, to just have your top-level program function, call it program, be pure, then you could have e.g.

main0 = program

Which would force all other functions below it to be pure. Using effmask if absolutely necessary - maybe have the compiler print warnings for these though.

Also, if main0 = pureProgram is too extreme, or if one is making a library, then either important portions of the program, or of the public API, could be made pure (or effectfully annotated) in the way that one wants to do.

Maybe this is even being done already by ATS programmers to some extent.

Best,

[Brandon Barker]

After sleeping on it, I realize part of my last email doesn't have much merit: namely the part about applications being able to enforce purity by using "pure" functions high up in the call stack  (e.g. program in that example); most of such functions are exactly the ones that need to be impure, due to having to also deal with IO.

Would it be possible to have the compiler allow the user to control the default effect type of functions?

[gmhwxi]

No such control as far as I know.

Personally, I feel that the design of effect-tracking in ATS2 is a failure.

I am not yet sure how to do it in ATS3. Or do it at all?

[Brandon Barker]

OK, Perhaps playing around with your Command code, and if needed, adding some extra syntax for it in ATS3, might be promising.

Incidentally, why is it needed to be a polymorphic function instead of a function template?

Belated apologies for hijacking this discussion.

[Hongwei Xi]

>>Incidentally, why is it needed to be a polymorphic function instead of a function template?

For otherwise the Bind constructor cannot be properly handled: The type variables 'a' and 'b'

are unknown at run-time.

--

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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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/1c4e3296-1c65-4685-b897-020bf297c5a7%40googlegroups.com.