Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

PoC for interface hierarchies #11978

Closed
cocreature opened this issue Dec 6, 2021 · 2 comments
Closed

PoC for interface hierarchies #11978

cocreature opened this issue Dec 6, 2021 · 2 comments
Assignees
@sofiafaro-da
Milestone
Daml Interfaces

Comments

@cocreature
Copy link
Contributor

No description provided.

@cocreature cocreature added this to the Daml Interfaces milestone Dec 6, 2021
@sofiafaro-da
Copy link
Contributor

sofiafaro-da commented Dec 6, 2021 •
edited
Loading

Idea is to have interfaces declare that other interfaces that are required, e.g.

interface B requires A where
  ...

So that when a template T implements interface B, the template T must also implement interface A:

template T
  with ...
  where
    ...
    implements A where ...
    implements B where ...

In LF, this means adding a repeated "requires" field in the interface definition, and checking that the required interface is correctly.

Additionally, we want to change EToInterface and EFromInterface to also allow converting between the interface B and its superinterface A, or introduce new expression forms that allow converting between an interface and its superinterfaces:

     A, B are typecons, 
     (A & B are interfaces and A is a superinterface of B),            // new case
     or (A is an interface and B is a template that implements it)     // existing case
     Γ  ⊢  e : B
   -------------------------------
     Γ  ⊢  EToInterface @A @B e : A 

     A, B are typecons, 
     (A & B are interfaces and A is a superinterface of B),            // new case
     or (A is an interface and B is a template that implements it)     // existing case
     Γ  ⊢  e : A
   -------------------------------
     Γ  ⊢  EFromInterface @A @B e : Optional B

Then in daml we expose everything as nicely as we can via typeclasses. E.g. we make sure that Implements B A is satisfied, so you can treat B as if it were a template that implements A.

sofiafaro-da added a commit that referenced this issue Dec 6, 2021
@sofiafaro-da
interfaces: Add requires in DefInterface protobuf
fce40bb 
Part of #11978

changelog_begin
changelog_end
@sofiafaro-da sofiafaro-da mentioned this issue Dec 6, 2021
Merged
7 tasks
sofiafaro-da added a commit that referenced this issue Dec 6, 2021
@sofiafaro-da
interfaces: Add requires in DefInterface protobuf
316bfa9 
Part of #11978

changelog_begin
changelog_end
sofiafaro-da added a commit that referenced this issue Dec 7, 2021
@sofiafaro-da
interfaces: Add requires in DefInterface protobuf (#11986)
9430ee3 
Part of #11978

changelog_begin
changelog_end
sofiafaro-da added a commit that referenced this issue Dec 7, 2021
@sofiafaro-da
interfaces: Add "requires" field in Haskell AST.
102f386 
Part of #11978. Adds typechecking for this on the interface and
implementation side.

changelog_begin
changelog_end
@sofiafaro-da sofiafaro-da mentioned this issue Dec 7, 2021
Merged
7 tasks
remyhaemmerle-da added a commit that referenced this issue Dec 7, 2021
@remyhaemmerle-da
LF: Add "requires" field to Scala Ast.
bb0375d 
Part of #11978. Adds typechecking for this field on the interface side,
and enforces that any template that implements A must implement B if A requires B.

CHANGELOG_BEGIN
CHANGELOG_END
@remyhaemmerle-da remyhaemmerle-da mentioned this issue Dec 7, 2021
Merged
7 tasks
sofiafaro-da added a commit that referenced this issue Dec 7, 2021
@sofiafaro-da
interfaces: add up/downcast expressions in proto
e409376 
Part of #11978

changelog_begin
changelog_end
@sofiafaro-da sofiafaro-da mentioned this issue Dec 7, 2021
Merged
7 tasks
sofiafaro-da added a commit that referenced this issue Dec 7, 2021
@sofiafaro-da
interfaces: Add "requires" field in Haskell AST. (#12016)
1dd8131 
* interfaces: Add "requires" field in Haskell AST.

Part of #11978. Adds typechecking for this on the interface and
implementation side.

changelog_begin
changelog_end

* Fix all the errors
remyhaemmerle-da added a commit that referenced this issue Dec 7, 2021
@remyhaemmerle-da
LF: Add "requires" field to Scala Ast. (#12028)
9d7eb07 
Part of #11978. Adds typechecking for this field on the interface side,
and enforces that any template that implements A must implement B if A requires B.

CHANGELOG_BEGIN
CHANGELOG_END
sofiafaro-da added a commit that referenced this issue Dec 7, 2021
@sofiafaro-da
interfaces: add up/downcast expressions in proto (#12030)
43c8641 
Part of #11978

changelog_begin
changelog_end
remyhaemmerle-da added a commit that referenced this issue Dec 8, 2021
@remyhaemmerle-da
LF: Add EToRequiredInterface and EFromRequiredInterface to Scala Ast.
d1a6c6c 
Part of #11978. Adds typechecking for those primitives.

CHANGELOG_BEGIN
CHANGELOG_END
@remyhaemmerle-da remyhaemmerle-da mentioned this issue Dec 8, 2021
Merged
7 tasks
remyhaemmerle-da added a commit that referenced this issue Dec 8, 2021
@remyhaemmerle-da
LF: Add EToRequiredInterface and EFromRequiredInterface to Scala Ast. (…
c53cf75 
…#12042)

Part of #11978. Adds typechecking for those primitives.

CHANGELOG_BEGIN
CHANGELOG_END
remyhaemmerle-da added a commit that referenced this issue Dec 8, 2021
@remyhaemmerle-da
Speey: Implement EToRequiredInterface and EFromRequiredInterface
b40f4d7 
Part of #11978. Adds typechecking for those primitives.

CHANGELOG_BEGIN
CHANGELOG_END
@remyhaemmerle-da remyhaemmerle-da mentioned this issue Dec 8, 2021
Merged
7 tasks
remyhaemmerle-da added a commit that referenced this issue Dec 8, 2021
@remyhaemmerle-da
Speedy: Implement EToRequiredInterface and EFromRequiredInterface
084a0a0 
Part of #11978.

CHANGELOG_BEGIN
CHANGELOG_END
remyhaemmerle-da added a commit that referenced this issue Dec 8, 2021
@remyhaemmerle-da
Speedy: Implement EToRequiredInterface and EFromRequiredInterface
d6241da 
Part of #11978.

CHANGELOG_BEGIN
CHANGELOG_END
remyhaemmerle-da added a commit that referenced this issue Dec 8, 2021
@remyhaemmerle-da
Speedy: Implement EToRequiredInterface and EFromRequiredInterface
bde0b76 
Part of #11978.

CHANGELOG_BEGIN
CHANGELOG_END
sofiafaro-da added a commit that referenced this issue Dec 8, 2021
@sofiafaro-da
interfaces: Add up/downcast in haskell AST
0455450 
Adds EToRequiredInterface and EFromRequiredInterface in
the Haskell AST, and the typechecker.

Part of #11978

changelog_begin
changelog_end
@sofiafaro-da sofiafaro-da mentioned this issue Dec 8, 2021
Merged
7 tasks
sofiafaro-da added a commit that referenced this issue Dec 8, 2021
@sofiafaro-da
interfaces: Add up/downcast in haskell AST (#12048)
04dd386 
Adds EToRequiredInterface and EFromRequiredInterface in
the Haskell AST, and the typechecker.

Part of #11978

changelog_begin
changelog_end
remyhaemmerle-da added a commit that referenced this issue Dec 8, 2021
@remyhaemmerle-da
Speedy: Implement EToRequiredInterface and EFromRequiredInterface (#1…
4f1892b 
…2046)

Part of #11978.

CHANGELOG_BEGIN
CHANGELOG_END
sofiafaro-da added a commit that referenced this issue Dec 8, 2021
@sofiafaro-da
interfaces: LFConversion support for requires
280bf39 
Part of #11978.
Adds a test that "requires" is enforced.

changelog_begin
changelog_end
@sofiafaro-da sofiafaro-da mentioned this issue Dec 8, 2021
Merged
7 tasks
sofiafaro-da added a commit that referenced this issue Dec 8, 2021
@sofiafaro-da
interfaces: LFConversion support for requires (#12055)
15020c9 
Part of #11978.
Adds a test that "requires" is enforced.

changelog_begin
changelog_end
sofiafaro-da added a commit that referenced this issue Dec 9, 2021
@sofiafaro-da
interfaces: Prevent circular and non-closed reqs
1a18fa4 
Updates the haskell side to be more strict about requirements:
- requirements must be transitively closed, so if A requires B, and B requires C,
  then A requires C.
- no circular requirements allowed

The logic for circular requirements is a bit duplicated to get a better
error message.

Part of #11978

changelog_begin
changelog_end
@sofiafaro-da sofiafaro-da mentioned this issue Dec 9, 2021
Merged
7 tasks
sofiafaro-da added a commit that referenced this issue Dec 9, 2021
@sofiafaro-da @cocreature
interfaces: Prevent circular and non-closed requirements. (#12073)
cbeab4b 
* interfaces: Prevent circular and non-closed reqs

Updates the haskell side to be more strict about requirements:
- requirements must be transitively closed, so if A requires B, and B requires C,
  then A requires C.
- no circular requirements allowed

The logic for circular requirements is a bit duplicated to get a better
error message.

Part of #11978

changelog_begin
changelog_end

* Update compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs

Co-authored-by: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>

* take a list in NotClosed error

Co-authored-by: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>
sofiafaro-da added a commit that referenced this issue Dec 9, 2021
@sofiafaro-da
interfaces: Support up/downcast in LFConversion
4b48587 
Part of #11978

changelog_begin
changelog_end
@sofiafaro-da sofiafaro-da mentioned this issue Dec 9, 2021
Merged
7 tasks
sofiafaro-da added a commit that referenced this issue Dec 9, 2021
@sofiafaro-da
interfaces: Support EToRequiredInterface and EFromRequiredInterface i…
0aacbac 
…n LFConversion (#12086)

* interfaces: Support up/downcast in LFConversion

Part of #11978

changelog_begin
changelog_end

* update TODO
realvictorprm pushed a commit that referenced this issue Dec 10, 2021
@sofiafaro-da @realvictorprm
interfaces: LFConversion support for requires (#12055)
bb2c347 
Part of #11978.
Adds a test that "requires" is enforced.

changelog_begin
changelog_end
realvictorprm pushed a commit that referenced this issue Dec 10, 2021
@sofiafaro-da @cocreature @realvictorprm
interfaces: Prevent circular and non-closed requirements. (#12073)
4321554 
* interfaces: Prevent circular and non-closed reqs

Updates the haskell side to be more strict about requirements:
- requirements must be transitively closed, so if A requires B, and B requires C,
  then A requires C.
- no circular requirements allowed

The logic for circular requirements is a bit duplicated to get a better
error message.

Part of #11978

changelog_begin
changelog_end

* Update compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs

Co-authored-by: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>

* take a list in NotClosed error

Co-authored-by: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>
realvictorprm pushed a commit that referenced this issue Dec 10, 2021
@sofiafaro-da @realvictorprm
interfaces: Support EToRequiredInterface and EFromRequiredInterface i…
c6d4986 
…n LFConversion (#12086)

* interfaces: Support up/downcast in LFConversion

Part of #11978

changelog_begin
changelog_end

* update TODO
sofiafaro-da added a commit that referenced this issue Dec 10, 2021
@sofiafaro-da
interfaces: Implement 'requires' syntax
96074ac 
part of: #11978

ghc counterpart: digital-asset/ghc#92

changelog_begin
changelog_end
@sofiafaro-da sofiafaro-da mentioned this issue Dec 10, 2021
Merged
7 tasks
sofiafaro-da added a commit that referenced this issue Dec 10, 2021
@sofiafaro-da
Add requires keyword for syntax highlighting
399901f 
Part of #11978

changelog_begin
changelog_end
@sofiafaro-da sofiafaro-da mentioned this issue Dec 10, 2021
Merged
7 tasks
sofiafaro-da added a commit that referenced this issue Dec 14, 2021
@sofiafaro-da
interfaces: Implement 'requires' syntax (#12105)
d1fb5e4 
* interfaces: Implement 'requires' syntax

part of: #11978

ghc counterpart: digital-asset/ghc#92

changelog_begin
changelog_end

* .

* ...

* ...

* ....

* ....

* update bazel-haskell-deps

* use requires syntax in tests

* .......

* .......

* update bazel-haskell-deps

* update InterfaceDesugared

* .........

* update bazel-haskell-deps

* ...........

* update bazel-haskell-depos

* update compile.yml

* update bazel-haskell-deps
sofiafaro-da added a commit that referenced this issue Dec 14, 2021
@sofiafaro-da
Add requires keyword for syntax highlighting (#12113)
7981379 
Part of #11978

changelog_begin
changelog_end
@sofiafaro-da
Copy link
Contributor

This proof-of-concept has been implemented.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@sofiafaro-da sofiafaro-da

Labels
None yet
Projects
None yet
Milestone
Daml Interfaces
Development

No branches or pull requests
2 participants
@cocreature @sofiafaro-da