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.

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

Test whether all derivations in MonoidalCategories type check using LazyCategories #16

Open
mohamed-barakat opened this issue Jan 19, 2022 · 2 comments

Comments

@mohamed-barakat
Copy link
Member

mohamed-barakat commented Jan 19, 2022

This is related to the bug fixed in homalg-project/CAP_project#804.

@zickgraf
Copy link
Member

For future reference: I have tried to do type checking during compilation (i.e. compare the syntax trees of the range of the pre morphism and the source of the post morphism in PreCompose) and in principle this works. However, there are lots of false positives because

  1. the compiler does not know about equalities in the specifications (e.g. Range( alpha ) = Source( beta ) in the specification of HomologyObject) and
  2. syntax trees can only be properly compared after everything is resolved and inlined. Currently, the compiler makes no guarantees about when this property is true for some subtree. Thus, the compiler sometimes compares partially resolved/inlined subtrees which usually are not equal as syntax trees.

For solving the first point, this equalities have to be given in a way readable for the compiler. For solving the second point I can imagine collecting all required equalities during compilation and defer the type checking until the end of the compilation when everything is guaranteed to be resolved and inlined.

zickgraf added a commit to zickgraf/CAP_project that referenced this issue Jan 24, 2022
See also homalg-project/LazyCategories#16 (comment)

For future reference: I have tried to do type checking during compilation (i.e. compare the syntax trees of the range of the pre morphism and the source of the post morphism in PreCompose) and in principle this works. However, there are lots of false positives because

    the compiler does not know about equalities in the specifications (e.g. Range( alpha ) = Source( beta ) in the specification of HomologyObject) and
    syntax trees can only be properly compared after everything is resolved and inlined. Currently, the compiler makes no guarantees about when this property is true for some subtree. Thus, the compiler sometimes compares partially resolved/inlined subtrees which usually are not equal as syntax trees.

For solving the first point, this equalities have to be given in a way readable for the compiler. For solving the second point I can imagine collecting all required equalities during compilation and defer the type checking until the end of the compilation when everything is guaranteed to be resolved and inlined.
@mohamed-barakat
Copy link
Member Author

This is now partially addressed in #19. However, I will keep this issue open for further future discussions.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants