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

Refactoring to support recursive capabilities #210

Merged
merged 1 commit into from
Aug 19, 2015
Merged

Refactoring to support recursive capabilities #210

merged 1 commit into from
Aug 19, 2015

Conversation

EliasC
Copy link
Contributor

@EliasC EliasC commented Aug 18, 2015

Before this commit, each occurrence of a ClassType stored its own
capability (implemented traits), but this turns out to be problematic.
Since a trait can be parameterized over a class type we can declare a
class as passive class C : T<C>, meaning that all occurrences of C
would indirectly store itself, thus leading to an infinite recursion.
The reason we didn't see any infinite loops is due to bugs when
resolving types. Fixing these, I managed to hang the compiler instead.

Here are some example programs exposing bugs in the current master,
which is fixed in this commit:

trait T<v>

passive class C<v> : T<v>
  f : C<int>
  def foo() : void
    this.f = new C<int>

Gives the error Type 'C<int>' does not match expected type 'C<int>' on
the last line. This is the bug that lead to this refactoring.

trait T<v>

passive class C : T<int, bool, string>

Compiles without complaining about the different number of type parameters.

passive class C : C

Crashes with the error encorec: Maybe.fromJust: Nothing

trait T<v>

passive class C<v> : T<C<v>>

class Main
  def main() : void
    let x = new C<int> : T<C<int>>
    in
      ()

Gives the error Type 'C<int>' does not match expected type 'T<C<int>>'
for the typecast in main (even though its a subtype). Will also hang
compilation if types are resolved properly.

Since we do not store capability information in the class types anymore,
checking for subtypes requires a lookup, which in turn means that
isSubtypeOf needs to be monadic. It has thus been moved to
Typechecker.Util, and has been extended to cover more cases. The
subtype checks in CodeGen.Expr has been simplified to
ty /= expected, optimistically trusting the typechecker that if two
types doesn't exactly match, it's safe to cast one into the other.

This commit also adds a verbatim mode to encorec (-v) that prints
the compiler phases before running them (useful for bug hunting, and
should probably be extended to become even more verbatimy in the
future).

It also captures the type constraints
(MonadError TCError m, MonadReader Environment m) in a type
TypecheckM a, meaning the type of all typechecking functions is now of
the form Foo -> TypecheckM Bar (where Bar is what the function
returns if there are no exceptions). This trick requires the ghc
extension Rank2Types, which has been added to the cabal file.

@albertnetymk
Copy link
Contributor

In Util.hs, getImplementedTraitscontains three guards on argument type. Two questions:

  1. In which cases, the argument would be a trait, first guard succeeds?
  2. Does it make sense to break those case into different functions? getImplementedTraits, I think, implies that the argument is a class, for only class implements traits.

@albertnetymk
Copy link
Contributor

Now Util.hs contains local functions, it should export public functions explicitly, right?

@EliasC
Copy link
Contributor Author

EliasC commented Aug 18, 2015

In Util.hs, getImplementedTraitscontains three guards on argument type. Two questions:
1 . In which cases, the argument would be a trait, first guard succeeds?

My thought was that you should be able to use the function regardless of the kind of ref type you have (UntypedRef excluded). I'm not sure this happens in currently in the code, but doing it like this, we could possibly avoid having one case for traits and one case for capabilities (for example).

2 . Does it make sense to break those case into different functions? getImplementedTraits, I think, implies that the argument is a class, for only class implements traits.

I would say that a trait implements itself trivially, and to some extent that a capability implements all its constituent traits (A + B * C implements A, B and C). When doing method dispatch on a reference type we need to get the same information regardless of the kind of ref type.

@EliasC
Copy link
Contributor Author

EliasC commented Aug 18, 2015

Now Util.hs contains local functions, it should export public functions explicitly, right?

Didn't think about it. Which ones do you think should be hidden?

@albertnetymk
Copy link
Contributor

I thought a trait can only be implemented by a class. The capability case is that a capability contains a collection of traits.

I fear that unifying the above cases would create some confusion. As for the first guard, getting the implemented traits from a trait, I can't think of any valid use cases. As for the third guard, getting the implemented traits from a capibility, traitsFromCapability does the job without using monad.

Went through all the usage of getImplementedTraits; the exact value constructor of Type is known before the function call.

When doing method dispatch on a reference type we need to get the same information regardless of the kind of ref type.

True; the only two things, I can think of, we can do on a ref type variable, is assignment and method call. subtypeOf should take care of the former and findMethod should take care of the latter, shouldn't they?

Which ones do you think should be hidden?

I was thinking about the monadic common functions, but maybe they would be used somewhere else.

@EliasC
Copy link
Contributor Author

EliasC commented Aug 18, 2015

I pushed a version with explicit exports now.

@EliasC
Copy link
Contributor Author

EliasC commented Aug 18, 2015

I thought a trait can only be implemented by a class. The capability case is that a capability contains a collection of traits.

Wouldn't it be more confusing to have a function getImplementedTraits that gets the traits from a ClassType and another function getContainedTraits that gets the traits from a CapabilityType? In the latest version getImplementedTraits is not exported from Util.hs, so maybe it's less of a problem?

I fear that unifying the above cases would create some confusion. As for the first guard, getting the implemented traits from a trait, I can't think of any valid use cases. As for the third guard, getting the implemented traits from a capibility, traitsFromCapability does the job without using monad.

I don't have any concrete usecases either, but I don't think that asking a trait type for its implemented traits should raise an error. It's not an absurd request. As for the third case, see below.

Went through all the usage of getImplementedTraits; the exact value constructor of Type is known before the function call.

Currently yes, but I was thinking of a hypothetical future use case that could have the following shape

foo ty 
  | isRefType ty
  , not (isUntypedRef ty) = do
      traits <- getImplementedTraits
      doAwesomeThingsWithTraits traits

rather than one case for each kind of ref type.

When doing method dispatch on a reference type we need to get the same information regardless of the kind of ref type.

True; the only two things, I can think of, we can do on a ref type variable, is assignment and method call. subtypeOf should take care of the former and findMethod should take care of the latter, shouldn't they?

Again, for the current version of the code I agree with you, but I don't see the harm in leaving that functionality. If I was tasked with writing a function that returns a list of all the traits whose interface a certain type provides, I would write it like this. Is getProvidedTraits a better name maybe?

@albertnetymk
Copy link
Contributor

Since it's a private function now, it's less of a problem.

I do feel having two functions, one for class type, the other for capability type, more clear. (I guess, it's more convincing if ClassType and CapabilityType are two different types, instead of two value constructors of the same type.)

Still, I would prefer the isTrait guard removed, for it's not used currently, and there are no obvious use cases where it could be used.

One drawback I can think of unifying these cases is that we lose the type info we obtained before calling the function. For sure, this is rather subjective. Anyway, my feeling is that we don't need to write functions as general as possible; instead, we could extend it when we actually need the extra feature, where we know more about what exactly is required.

Before this commit, each occurrence of a `ClassType` stored its own
capability (implemented traits), but this turns out to be problematic.
Since a trait can be parameterized over a class type we can declare a
class as `passive class C : T<C>`, meaning that all occurrences of `C`
would indirectly store itself, thus leading to an infinite recursion.
The reason we didn't see any infinite loops is due to bugs when
resolving types. Fixing these, I managed to hang the compiler instead.

Here are some example programs exposing bugs in the current master,
which is fixed in this commit:

```
trait T<v>

passive class C<v> : T<v>
  f : C<int>
  def foo() : void
    this.f = new C<int>
```
Gives the error `Type 'C<int>' does not match expected type 'C<int>'` on
the last line. This is the bug that lead to this refactoring.

```
trait T<v>

passive class C : T<int, bool, string>
```
Compiles without complaining about the different number of type parameters.

```
passive class C : C
```
Crashes with the error `encorec: Maybe.fromJust: Nothing`

```
trait T<v>

passive class C<v> : T<C<v>>

class Main
  def main() : void
    let x = new C<int> : T<C<int>>
    in
      ()
```
Gives the error `Type 'C<int>' does not match expected type 'T<C<int>>'`
for the typecast in `main` (even though its a subtype). Will also hang
compilation if types are resolved properly.

Since we do not store capability information in the class types anymore,
checking for subtypes requires a lookup, which in turn means that
`isSubtypeOf` needs to be monadic. It has thus been moved to
`Typechecker.Util`, and has been extended to cover more cases. The
subtype checks in `CodeGen.Expr` has been simplified to
`ty /= expected`, optimistically trusting the typechecker that if two
types doesn't exactly match, it's safe to cast one into the other.

This commit also adds a verbatim mode to `encorec` (`-v`) that prints
the compiler phases before running them (useful for bug hunting, and
should probably be extended to become even more verbatimy in the
future).

It also captures the type constraints
`(MonadError TCError m, MonadReader Environment m)` in a type
`TypecheckM a`, meaning the type of all typechecking functions is now of
the form `Foo -> TypecheckM Bar` (where `Bar` is what the function
returns if there are no exceptions). This trick requires the ghc
extension `Rank2Types`, which has been added to the cabal file.
@EliasC
Copy link
Contributor Author

EliasC commented Aug 18, 2015

Okay, you made some fair points. The latest version only uses getImplementedTraits for classes (which turns out to be only once in subtypeOf right now) and the non-monadic traitsFromCapability for capabilities.

@albertnetymk
Copy link
Contributor

I think it can be merged. No objections?

@kikofernandez
Copy link
Contributor

no objections

kikofernandez pushed a commit that referenced this pull request Aug 19, 2015
Refactoring to support recursive capabilities
@kikofernandez kikofernandez merged commit 1600e4f into parapluu:master Aug 19, 2015
@kikofernandez kikofernandez deleted the fix/recursive-types branch August 19, 2015 06:11
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

Successfully merging this pull request may close these issues.

3 participants