aya-prover / aya-prover-proto

┗:smiley:┛ ┏:smiley:┓ ┗:smiley:┛
GNU General Public License v3.0
11 stars 0 forks source link

Slogan #61

Closed tonyxty closed 3 years ago

tonyxty commented 3 years ago

How about "safe things should be safe, unsafe things possible"

Also we should decide whether we encourage "there is one way to do one thing" or do we encourage multiple way to do one thing? I vote for the former, and I think we should decide on this ASAP since it affects many design choices.

ice1000 commented 3 years ago

I agree on

How about "safe things should be safe, unsafe things possible"

and

I vote for the former

but I think the slogan should be more informative. Maybe create docs/design-choices.md that talks about our preference or standard when making choices, and amend it on-demand.

re-xyr commented 3 years ago

Also a question would be whether we will support side effects with something like IO (as in Haskell, etc) or directly allow impurity (as in OCaml, etc) in unsafe mzi.

tonyxty commented 3 years ago

Maybe create docs/design-choices.md that talks about our preference or standard when making choices, and amend it on-demand.

Great, I'll put these two sentences there first.

ice1000 commented 3 years ago

Also a question would be whether we will support side effects with something like IO (as in Haskell, etc) or directly allow impurity (as in OCaml, etc) in unsafe mzi.

Can I say ;; is the >>= operator for the Unsafe monad?

re-xyr commented 3 years ago

Also a question would be whether we will support side effects with something like IO (as in Haskell, etc) or directly allow impurity (as in OCaml, etc) in unsafe mzi.

Can I say ;; is the >>= operator for the Unsafe monad?

I thought ;; does not need lifting (or, automatically lifts)?

ice1000 commented 3 years ago

Also a question would be whether we will support side effects with something like IO (as in Haskell, etc) or directly allow impurity (as in OCaml, etc) in unsafe mzi.

Can I say ;; is the >>= operator for the Unsafe monad?

I thought ;; does not need lifting (or, automatically lifts)?

Yes, that's even more convenient

re-xyr commented 3 years ago

Also a question would be whether we will support side effects with something like IO (as in Haskell, etc) or directly allow impurity (as in OCaml, etc) in unsafe mzi.

Can I say ;; is the >>= operator for the Unsafe monad?

I thought ;; does not need lifting (or, automatically lifts)?

Yes, that's even more convenient

Will there be occasions where we want unlifted IOs? Also, what will be the evaluation strategy?

ice1000 commented 3 years ago

Also a question would be whether we will support side effects with something like IO (as in Haskell, etc) or directly allow impurity (as in OCaml, etc) in unsafe mzi.

Can I say ;; is the >>= operator for the Unsafe monad?

I thought ;; does not need lifting (or, automatically lifts)?

Yes, that's even more convenient

Will there be occasions where we want unlifted IOs? Also, what will be the evaluation strategy?

An unlifted IO can be seen as a unified monad with the capabilities of throwing exceptions and use STRefs and doing IO and modifying the heap. And that is that.

Evaluation strategy? We don't evaluate IO at compile time. At runtime, I don't know. Maybe we can implement a Haskellish lazy evaluation, or make it fast by being strict.