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

Existential types support #1066

Merged
merged 28 commits into from
Nov 23, 2023
Merged

Existential types support #1066

merged 28 commits into from
Nov 23, 2023

Conversation

johnynek
Copy link
Owner

@johnynek johnynek commented Oct 31, 2023

closes #651

@codecov-commenter
Copy link

codecov-commenter commented Oct 31, 2023

Codecov Report

Attention: 31 lines in your changes are missing coverage. Please review.

Comparison is base (7e044b9) 92.03% compared to head (b418a5c) 92.35%.
Report is 1 commits behind head on master.

❗ Current head b418a5c differs from pull request most recent head 7f4fefa. Consider uploading reports for the commit 7f4fefa to get more accurate results

Files Patch % Lines
.../src/main/scala/org/bykn/bosatsu/rankn/Infer.scala 92.68% 15 Missing ⚠️
...e/src/main/scala/org/bykn/bosatsu/rankn/Type.scala 96.75% 6 Missing ⚠️
...main/scala/org/bykn/bosatsu/TypedExprToProto.scala 91.83% 4 Missing ⚠️
...re/src/main/scala/org/bykn/bosatsu/TypedExpr.scala 97.33% 4 Missing ⚠️
...e/src/main/scala/org/bykn/bosatsu/TypeParser.scala 93.75% 1 Missing ⚠️
...cala/org/bykn/bosatsu/TypedExprNormalization.scala 93.33% 1 Missing ⚠️

❗ Your organization needs to install the Codecov GitHub app to enable full functionality.

Additional details and impacted files
@@            Coverage Diff             @@
##           master    #1066      +/-   ##
==========================================
+ Coverage   92.03%   92.35%   +0.31%     
==========================================
  Files          93       93              
  Lines        9903    10277     +374     
  Branches     2319     2390      +71     
==========================================
+ Hits         9114     9491     +377     
+ Misses        789      786       -3     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@johnynek johnynek changed the title Adds parsing, but not inference or type checking, or existential types. Existential types support Nov 21, 2023
@@ -41,6 +41,12 @@ message TypeForAll {
int32 typeValue = 3;
}

message TypeExists {
repeated int32 varNames = 1;
repeated Kind kinds = 2;
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should use VarKind like generic

@@ -32,9 +35,14 @@ abstract class TypeParser[A] {
(maybeSpacesAndLines.soft.with1 *> (P.char(':') *> maybeSpacesAndLines *> Kind.parser))
lowerIdent ~ kindP.?
}

val univLike: P[(NonEmptyList[(String, Option[Kind])], A) => A] =
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Quantified is a better name.

def setInf(inf: Expected.Inf[(Type.Rho, Region)], rho: Type.Rho, r: Region): Infer[Unit] =
lift(inf.ref.update[Infer[Unit]] {
case Left(_) => (Right((rho, r)), unit)
case right@Right((rho1, r1)) => (right, unify(rho1, rho, r1, r))
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems we never hit this branch so the code only solves one or zero times for each variable which is what we would hope.

Probably revert this change.

@@ -993,23 +1238,29 @@ object Infer {
// are missing here.
inferSigma(term)
.flatMap { tsigma =>
assertNoFree(tsigma.getType, s"line 1160 from $term\n\n${tsigma.repr}")
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's remove these assertions since they were defensive and now pass.

@@ -1098,7 +1351,8 @@ object Infer {
*
* TODO: Pattern needs to have a region for each part
*/
def typeCheckPattern(pat: Pattern, sigma: Expected.Check[(Type, Region)], reg: Region): Infer[(Pattern, List[(Bindable, Type)])] =
def typeCheckPattern(pat: Pattern, sigma: Expected.Check[(Type, Region)], reg: Region): Infer[(Pattern, List[(Bindable, Type)])] = {
assertNoFree(sigma.value._1, "in typeCheckPattern line 1266")
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Remove defensive check.

val boundSet = q.vars.iterator.map(_._1).toSet[Type.Var]
val env1 = env.iterator.filter { case (v, _) => !boundSet(v) }.toMap
val subin = substituteVar(q.in, env1)
forAll(q.forallList, exists(q.existList, subin))
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should be able to directly uses quantify.

val forAllSize = fa1.size
val normfas = newVars.take(forAllSize)
val normexs = newVars.drop(forAllSize)
forAll(normfas, Type.exists(normexs, normin))
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be able to use quantify here I think.

}
case q: Quantified =>
val varList = q.vars.toList
require(varList.size == varList.toMap.size, s"invalid q: $q")
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This passes we can remove now.

sys.error(s"illegal skolem ($t) escape in ${te.repr}")
case Type.TyVar(Type.Var.Bound(_)) => t
/*
this doesn't work correctly with traverseType
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Remove commented code.

@johnynek johnynek merged commit e39f11a into master Nov 23, 2023
13 checks passed
@johnynek johnynek deleted the oscar/20231026_existential_quant branch November 23, 2023 23:16
@johnynek johnynek restored the oscar/20231026_existential_quant branch November 23, 2023 23:16
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.

document or add support for existential quantification
2 participants