Parametric signatures?

[dbp]

We have parametric contracts, though they have to be made concrete on use. Is it feasible to add contract variables? i.e., I can write:

(define-contract (Maybe T) (OneOf T (Constant #f))))

Which is great, but I can't (as far as I know!), write:

(: map (-> (-> X Y) (List X) (List Y)))
...

[camoy]

It's not supported at the moment, but we can do this. One possible interpretation of the contract variables is just to replace them with Any. That's easy, but not enforcing anything like parametricity. The "correct" way to do it is to perform sealing at negative positions and unsealing at positive positions (as in Arjun's paper). Of course, this means violations of parametricity yield a weird run-time error (e.g. expected: integer? got: #<seal>). Thoughts on what makes more sense for us?

[dbp]

I think doing sealing makes sense. As long as the blame is decent, the error will make enough sense (once explained) and the alternative is pretty crappy (it’s how Sperbers checked signatures worked, and I didn’t like it in fundies 1, so really don’t think it’ll be great for Logic…)

On Fri, Dec 22, 2023, at 5:01 PM, Cameron Moy wrote:

It's not supported at the moment, but we can do this. One possible interpretation of the contract variables is just to replace them with Any. That's easy, but not enforcing anything like parametricity. The "correct" way to do it is to perform sealing at negative positions and unsealing at positive positions (as in Arjun's paper https://cs.brown.edu/people/aguha/papers/guha-dls2007.pdf). Of course, this means violations of parametricity yield a weird run-time error (e.g. expected: integer? got: #<seal>). Thoughts on what makes more sense for us?

— Reply to this email directly, view it on GitHub https://github.com/logiccomp/lsl/issues/9#issuecomment-1868095997, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAELBJPEA2GENJXI26VWRI3YKX7MLAVCNFSM6AAAAABBAGE3TSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNRYGA4TKOJZG4. You are receiving this because you authored the thread.Message ID: @.***>

[camoy]

If we're doing parametric contracts, then it's trivial to add in existential contracts as well. You could then do parametricity, data abstraction, capabilities, and other related topics in class perhaps.

[dbp]

All those things would be wonderful to be able to cover.

On Sat, Dec 23, 2023, at 5:22 PM, Cameron Moy wrote:

If we're doing parametric contracts, then it's trivial to add in existential contracts https://docs.racket-lang.org/guide/contracts-exists.html as well. You could then do parametricity, data abstraction, capabilities, and other related topics in class perhaps.

— Reply to this email directly, view it on GitHub https://github.com/logiccomp/lsl/issues/9#issuecomment-1868380322, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAELBJJ4YOOYJCMSPFBRD5TYK5KTXAVCNFSM6AAAAABBAGE3TSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNRYGM4DAMZSGI. You are receiving this because you authored the thread.Message ID: @.***>