Re: proofs vs statics?
No, a proof is not a type. A proof is a total program (that is pure and terminating). On Friday, March 22, 2019 at 1:55:17 PM UTC-4, Yannick Duchêne wrote: > > Within ATS, is it correct to say a proof is usually a dependant type? > (whose value just get discarded from the generated program). > > > P.S. Just wanted to have a quick look at some interesting talk here. > Unfortunately, I still don’t have time to get back at ATS. > -- 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/c176e9d3-bd56-40b4-a722-32879f28e923%40googlegroups.com.
Re: Referential transparency in ATS
Sounds like I have to fix atspkg :p If you want to use the monads package with npm + Makefiles, I suppose I could upload to npm (it might even be a good idea given the permanence of packages there). As an aside: I suspect that what makes IO so nice in the context of Haskell is that you get the same result for the same inputs, every time. It turns out that many operations involving reads/writes to memory still satisfy this - and one would like to be able to express that, though I suspect it would be difficult. Cheers, Vanessa McHale On 3/23/19 2:06 PM, Brandon Barker wrote: > > > On Friday, March 22, 2019 at 2:49:29 PM UTC-4, Brandon Barker wrote: > > Hey Artyom, > > Thanks for the very interesting analysis and response. > > On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov > mailto:artyom.shalkha...@gmail.com>> > wrote: > > Hi Brandon, > > This is a very lively discussion, thanks for bringing it up. > > On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker > wrote: > > And for what it's worth, here is an Idris program for haha > using Effects: > > | > moduleMain > > > importEffects > importEffect.StdIO > > > hello :Eff()[STDIO] > hello =let ha =StdIO.putStr "ha"inha *>ha > > > main :IO () > main =run hello > > | > > > It prints "ha" twice, despite being a strict language. I > presume, but am not sure, this is because the effect time > requires it to be re-evaluated each time. > > > > Well, the type of "hello" says that the computation will use > the STDIO effect as many times as is necessary. The way the > computation is constructed, it is meant to issue commands in a > given sequence. > > One peculiarity of PureScript is that of handling effects via > the algebraic effects approach. It's not easy to do in a > high-performance way, because you need a call/cc construct > present in the language, and moreover a 'multi-shot' one at > that (i.e. the continuation *may* be invoked zero, once or > more times by the effect interpreter). In ATS a simpler way is > to use template functions to define effects differently (e.g. > during testing and during the actual execution) -- it's > constrained compared to the call/cc for sure, but then you > don't have to pay the price of the call/cc plumbing. Another > thing about PureScript is that it uses row types to track the > set of effects that a given Eff computation may involve during > its evaluation. > > > Not that it will invalidate anything you just said, but the above > code was Idris, but they may be similar in this regard (not sure). > I need to look into call/cc more at some point - not very familiar > with this idea. But I like where you are going with templates in ATS! > > > So in short, if we view the programs as creating commands, and > then some kind of external interpreter that executes them, > then it all matches up. The programs might be quite pure and > non-side-effecting (except for non-termination aka infinite > looping runtime exceptions), the interpreter will perform the > effects. Here's a pseudocode for the interpreter: > > // the command sub-language > datatype Command = Print of string | Nop | Seq of (command, > command) > extern > fun runCommand (c:Command): void > extern > fun seq (c:Command, Command): Command > extern > fun cprint (s:string): Command > implement > seq (c1, c2) = Seq (c1, c2) > implement > cprint (s) = Print s > // the interpreter itself > implement > runCommand (c) = case+ c of Nop => (*done!*) | Print s => > print (s) | Seq (c1, c2) => (runCommand(c1); runCommand(c2)) > > Now let's assume the Command is abstract for the rest of the > program (and only the runCommand, seq and print are exposed). > We can now write: > > val hello = let val h = cprint "hi" in seq (h, h) end // here. > twice the effect! > implement > main0 () = runCommand hello > > The "hello" itself is free of side-effects (or so it seems to > me!). We might need to lazily evaluate stuff here (e.g. to > enable looping, where you need to give the interpreter the > chance to run side-by-side with your expression). Or we need a > more poweful "seq" (i.e. the Haskell's "bind" operator for > stitching together the commands such that the left-hand side > has to be evaluated to a value that is then fed to the > right-hand side -- i.e. incrementally built-up as it's being > evaluated by
Re: Referential transparency in ATS
On Friday, March 22, 2019 at 2:49:29 PM UTC-4, Brandon Barker wrote: > > Hey Artyom, > > Thanks for the very interesting analysis and response. > > On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov < > artyom.shalkha...@gmail.com> wrote: > >> Hi Brandon, >> >> This is a very lively discussion, thanks for bringing it up. >> >> On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote: >>> >>> And for what it's worth, here is an Idris program for haha using Effects: >>> >>> module Main >>> >>> >>> import Effects >>> import Effect.StdIO >>> >>> >>> hello : Eff () [STDIO] >>> hello = let ha = StdIO.putStr "ha" in ha *> ha >>> >>> >>> main : IO () >>> main = run hello >>> >>> >>> >>> It prints "ha" twice, despite being a strict language. I presume, but am >>> not sure, this is because the effect time requires it to be re-evaluated >>> each time. >>> >>> >>> >> Well, the type of "hello" says that the computation will use the STDIO >> effect as many times as is necessary. The way the computation is >> constructed, it is meant to issue commands in a given sequence. >> >> One peculiarity of PureScript is that of handling effects via the >> algebraic effects approach. It's not easy to do in a high-performance way, >> because you need a call/cc construct present in the language, and moreover >> a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero, >> once or more times by the effect interpreter). In ATS a simpler way is to >> use template functions to define effects differently (e.g. during testing >> and during the actual execution) -- it's constrained compared to the >> call/cc for sure, but then you don't have to pay the price of the call/cc >> plumbing. Another thing about PureScript is that it uses row types to track >> the set of effects that a given Eff computation may involve during its >> evaluation. >> > > Not that it will invalidate anything you just said, but the above code was > Idris, but they may be similar in this regard (not sure). I need to look > into call/cc more at some point - not very familiar with this idea. But I > like where you are going with templates in ATS! > >> >> So in short, if we view the programs as creating commands, and then some >> kind of external interpreter that executes them, then it all matches up. >> The programs might be quite pure and non-side-effecting (except for >> non-termination aka infinite looping runtime exceptions), the interpreter >> will perform the effects. Here's a pseudocode for the interpreter: >> >> // the command sub-language >> datatype Command = Print of string | Nop | Seq of (command, command) >> extern >> fun runCommand (c:Command): void >> extern >> fun seq (c:Command, Command): Command >> extern >> fun cprint (s:string): Command >> implement >> seq (c1, c2) = Seq (c1, c2) >> implement >> cprint (s) = Print s >> // the interpreter itself >> implement >> runCommand (c) = case+ c of Nop => (*done!*) | Print s => print (s) | Seq >> (c1, c2) => (runCommand(c1); runCommand(c2)) >> >> Now let's assume the Command is abstract for the rest of the program (and >> only the runCommand, seq and print are exposed). We can now write: >> >> val hello = let val h = cprint "hi" in seq (h, h) end // here. twice the >> effect! >> implement >> main0 () = runCommand hello >> >> The "hello" itself is free of side-effects (or so it seems to me!). We >> might need to lazily evaluate stuff here (e.g. to enable looping, where you >> need to give the interpreter the chance to run side-by-side with your >> expression). Or we need a more poweful "seq" (i.e. the Haskell's "bind" >> operator for stitching together the commands such that the left-hand side >> has to be evaluated to a value that is then fed to the right-hand side -- >> i.e. incrementally built-up as it's being evaluated by the interpeter). >> >> In Haskell, the type Command is termed "IO" (with an additional type >> parameter to signify the result type of the command) and the interpreter is >> somewhere in the runtime system. >> > > Nice to see that the basis of an interpreter can be created so easily! I > guess to make it feasible to program in, in addition to the issues you just > mentioned, some primitive standard library functions would need to be > wrapped up as 'Command' functions just as you did with cprint; another way > to do this might be to ascribe certain effect types to these primitives > using e.g praxi. Functions that build on these primitives could then > accumulate effects - perhaps some effects could even be consumed, but not > sure. Also not sure how the interpreter would deal with some values have > more than one effect type: Haskell seems to use the idea of monad > transformers to get around this but I do not find it particularly > satisfying so far > > Still need to look into effects and how to encode different effect types - > I seem to recall ATS actually had build in support for effects at the type > level at some
