search

diprism / perpl

The PERPL Compiler
MIT License
10 stars 5 forks source link

More syntax of ampersand #22

Closed davidweichiang closed 2 years ago

davidweichiang commented 3 years ago

Currently we don't have a tuple type, but they are "fused" into datatypes, i.e., you'd have to write

data Pair Nat Nat
let x = Pair Zero Zero

for a pair (0,0)

So it seems kind of asymmetric that ampersand-products would be created using angle brackets, i.e., <Zero, Zero>. Are we okay with that? Or do we want to find an alternative?

We could also add expressions like (Zero, Zero)?

davidweichiang commented 3 years ago

On further thought, I think we need tuples with parens. For example, in pda.ppl, we have to create a datatype for SymbolxState when it would be a lot more convenient just to have Symbol * State.

davidweichiang commented 2 years ago

Another question is how ampersand interacts with probabilities. The simplest test-case we came up with was

<true, fail>.1

Should this evaluate to true (with weight 1) or should it fail?

davidweichiang commented 2 years ago

Depending on the answer to the above, the translation to FGG might or might not be right. If the above should fail, then the rules need another e2 or e1 on the rhs that goes to nowhere.

davidweichiang commented 2 years ago

What is amb_{a&b} where a and b are types?

(I'm just typing in all the questions that are coming up in my meeting with @HerbertMcSnout, for discussion tomorrow.)

davidweichiang commented 2 years ago

Possibly a more basic issue is, since our definition of linearity is "every function is called exactly once," this term should not typecheck:

<\lambda x.x, \lambda x.x>

It's only under the notion of linearity "every variable is used exactly once" that this term would be typable.

ccshan commented 2 years ago

There's some kind of property cluster (read: I'm having trouble recalling the exact logical reasoning) that says the two parts of an ampersand angle-bracket pair are like the two branches of an if....

davidweichiang commented 2 years ago

ftr: https://pdf.sciencedirectassets.com/271538/1-s2.0-S0304397500X04045/1-s2.0-030439759390181R/main.pdf

colin-mcd commented 2 years ago

We discussed on Thursday Nov. 4 that we wanted let _ = <fail : A, fail : B> in ... to not fail. This is straightforward to implement, but I was surprised by the consequence then that <fail : A, fail : B> != fail : A & B because let _ = fail : A & B in ... should fail (right?). Is this what you would expect?

davidweichiang commented 2 years ago

i think so?

ccshan commented 2 years ago

I think so too.