Skip to content

Commit

Permalink
experimental implementation of do notation
Browse files Browse the repository at this point in the history
  • Loading branch information
sergei.winitzki committed Nov 22, 2023
1 parent cd15b03 commit fb2c442
Show file tree
Hide file tree
Showing 4 changed files with 101 additions and 5 deletions.
34 changes: 34 additions & 0 deletions scall-core/src/main/scala/io/chymyst/ui/dhall/Parser.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import io.chymyst.ui.dhall.Syntax.ExpressionScheme._
import io.chymyst.ui.dhall.Syntax._
import io.chymyst.ui.dhall.Syntax.{DhallFile, Expression, ExpressionScheme, PathComponent, RawRecordLiteral}
import io.chymyst.ui.dhall.SyntaxConstants.{ConstructorName, FieldName, ImportType, VarName}
import io.chymyst.ui.dhall.TypeCheck._Type
import jdk.jfr.Experimental

import java.io.InputStream
Expand Down Expand Up @@ -880,6 +881,35 @@ object Grammar {
letBindings.foldRight(expr) { case ((varName, tipe, body), prev) => Let(varName, tipe, body, prev) }
}

// Experimental: "do notation"
// "as (M A) in bind with x : B in p with y : C in q then z"
def expression_as_in[$: P]: P[Expression] = P(
requireKeyword("as") ~ whsp1 ~/ application_expression ~ whsp ~
requireKeyword("in") ~ whsp1 ~/ expression ~ whsp ~
with_binding.rep(1) ~ requireKeyword("then") ~ whsp1 ~ expression
).map { case (Expression(Application(typeConstructor, typeArg)), bind, withBindings, thenResult) =>
// Desugar according to https://discourse.dhall-lang.org/t/proposal-do-notation-syntax/99
// as (M A) in bind ... with x : B in q <rest>
// desugars to
// bind B A q (\(x: B) -> desugar <rest> )
//
// as (M A) in bind ...then q <end of construction>
// desugars to
// ... -> q
val varA = ~"a"
val varB = ~"b"

val bindWithTypeAnnotation = bind | ((varA | _Type) ->: (varB | _Type) ->: typeConstructor(varA) ->: ((~"_" | varA) ->: typeConstructor(varB)) ->: typeConstructor(varB))

withBindings.foldRight(thenResult) { case ((varName, varType, source), b) => bindWithTypeAnnotation(varType)(typeArg)(source)((~(varName.name) | varType) -> b) }
}

// A part of the do-notation syntax: "with x : B in p".
// The type annotation is required because we will then desugar to a Lambda where a type annotation is required, and it's too early for type inference.
def with_binding[$: P]: P[(VarName, Expression , Expression)] = P(
requireKeyword("with") ~ whsp1 ~/ nonreserved_label ~ whsp ~ ":" ~ whsp1 ~/ expression ~ whsp ~ requireKeyword("in") ~ whsp1 ~/ expression ~ whsp
)

def expression_forall[$: P]: P[Expression] = P(forall ~ whsp ~/ "(" ~ whsp ~ nonreserved_label ~ whsp ~/ ":" ~ whsp1 ~/ expression ~ whsp ~ ")" ~ whsp ~ arrow ~/
whsp ~ expression)
.map { case (varName, tipe, body) => Forall(varName, tipe, body) }
Expand Down Expand Up @@ -915,6 +945,10 @@ object Grammar {
// "forall (x : a) -> b"
| NoCut(expression_forall)
//
// Experimental: "do notation"
// "as (M A) in bind with x : B in p with y : C in q then z"
| NoCut(expression_as_in)
//
// "a -> b"
//
// NOTE: Backtrack if parsing this alternative fails
Expand Down
2 changes: 1 addition & 1 deletion scall-core/src/main/scala/io/chymyst/ui/dhall/Syntax.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -934,7 +934,7 @@ object Syntax {
case _ => throw new Exception(s"Invalid lambda in DSL: base must be an Annotation with zero-index variable but is ${this.toDhall}: $this")
}

// Forall type expressions.
// Forall type expressions. The argument must be an annotation.
def ->:(tipe: Expression): Expression = tipe.scheme match {
case Annotation(Expression(Variable(name, index)), t) if index == 0 => Forall(name, t, this)
case _ => Forall(underscore, tipe, this)
Expand Down
16 changes: 15 additions & 1 deletion scall-core/src/test/scala/io/chymyst/ui/dhall/unit/SimpleExpressionTest.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ import io.chymyst.ui.dhall.SyntaxConstants.Builtin.Natural
import io.chymyst.ui.dhall.SyntaxConstants.FilePrefix.Here
import io.chymyst.ui.dhall.SyntaxConstants.ImportMode.{Code, RawText}
import io.chymyst.ui.dhall.SyntaxConstants.ImportType.{Env, Missing, Path}
import io.chymyst.ui.dhall.SyntaxConstants.{ConstructorName, FieldName, File, VarName}
import io.chymyst.ui.dhall.SyntaxConstants.{Builtin, Constant, ConstructorName, FieldName, File, VarName}
import io.chymyst.ui.dhall._
import io.chymyst.ui.dhall.unit.TestUtils.{check, toFail, v}
import munit.FunSuite
Expand Down Expand Up @@ -317,4 +317,18 @@ class SimpleExpressionTest extends FunSuite {
val input = "./path0/path1/path2/file"
check(Grammar.import_expression(_), input, Expression(Import(Path(Here, File(List("path0", "path1", "path2", "file"))), Code, None)))
}

test("do notation") {
val input =
"""as List Natural in bind
| with x : Bool in q
| with y : Integer in r
| with z : Text in s
| then k
|""".stripMargin

val expected: Expression = Expression(Application(Expression(Application(Expression(Application(Expression(Application(Expression(Annotation(Expression(Variable(VarName("bind"),0)),Expression(Forall(VarName("a"),Expression(ExprConstant(Constant.Type)),Expression(Forall(VarName("b"),Expression(ExprConstant(Constant.Type)),Expression(Forall(VarName("_"),Expression(Application(Expression(ExprBuiltin(Builtin.List)),Expression(Variable(VarName("a"),0)))),Expression(Forall(VarName("_"),Expression(Forall(VarName("_"),Expression(Variable(VarName("a"),0)),Expression(Application(Expression(ExprBuiltin(Builtin.List)),Expression(Variable(VarName("b"),0)))))),Expression(Application(Expression(ExprBuiltin(Builtin.List)),Expression(Variable(VarName("b"),0)))))))))))))),Expression(ExprBuiltin(Builtin.Bool)))),Expression(ExprBuiltin(Natural)))),Expression(Variable(VarName("q"),0)))),Expression(Lambda(VarName("x"),Expression(ExprBuiltin(Builtin.Bool)),Expression(Application(Expression(Application(Expression(Application(Expression(Application(Expression(Annotation(Expression(Variable(VarName("bind"),0)),Expression(Forall(VarName("a"),Expression(ExprConstant(Constant.Type)),Expression(Forall(VarName("b"),Expression(ExprConstant(SyntaxConstants.Constant.Type)),Expression(Forall(VarName("_"),Expression(Application(Expression(ExprBuiltin(Builtin.List)),Expression(Variable(VarName("a"),0)))),Expression(Forall(VarName("_"),Expression(Forall(VarName("_"),Expression(Variable(VarName("a"),0)),Expression(Application(Expression(ExprBuiltin(Builtin.List)),Expression(Variable(VarName("b"),0)))))),Expression(Application(Expression(ExprBuiltin(Builtin.List)),Expression(Variable(VarName("b"),0)))))))))))))),Expression(ExprBuiltin(Builtin.Integer)))),Expression(ExprBuiltin(Natural)))),Expression(Variable(VarName("r"),0)))),Expression(Lambda(VarName("y"),Expression(ExprBuiltin(Builtin.Integer)),Expression(Application(Expression(Application(Expression(Application(Expression(Application(Expression(Annotation(Expression(Variable(VarName("bind"),0)),Expression(Forall(VarName("a"),Expression(ExprConstant(Constant.Type)),Expression(Forall(VarName("b"),Expression(ExprConstant(Constant.Type)),Expression(Forall(VarName("_"),Expression(Application(Expression(ExprBuiltin(Builtin.List)),Expression(Variable(VarName("a"),0)))),Expression(Forall(VarName("_"),Expression(Forall(VarName("_"),Expression(Variable(VarName("a"),0)),Expression(Application(Expression(ExprBuiltin(Builtin.List)),Expression(Variable(VarName("b"),0)))))),Expression(Application(Expression(ExprBuiltin(Builtin.List)),Expression(Variable(VarName("b"),0)))))))))))))),Expression(ExprBuiltin(Builtin.Text)))),Expression(ExprBuiltin(Natural)))),Expression(Variable(VarName("s"),0)))),Expression(Lambda(VarName("z"),Expression(ExprBuiltin(Builtin.Text)),Expression(Variable(VarName("k"),0))))))))))))))
check(Grammar.expression_as_in(_), input, expected)
expect(expected.toDhall == "bind: (∀(a: Type) -> ∀(b: Type) -> ∀(_: List a) -> ∀(_: ∀(_: a) -> List b) -> List b) Bool Natural q (λ(x: Bool) -> bind: (∀(a: Type) -> ∀(b: Type) -> ∀(_: List a) -> ∀(_: ∀(_: a) -> List b) -> List b) Integer Natural r (λ(y: Integer) -> bind: (∀(a: Type) -> ∀(b: Type) -> ∀(_: List a) -> ∀(_: ∀(_: a) -> List b) -> List b) Text Natural s (λ(z: Text) -> k)))")
}
}
54 changes: 51 additions & 3 deletions scall-core/src/test/scala/io/chymyst/ui/dhall/unit/SimpleSemanticsTest.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@ import com.eed3si9n.expecty.Expecty.expect
import io.chymyst.ui.dhall.Parser.InlineDhall
import io.chymyst.ui.dhall.Syntax.Expression._
import io.chymyst.ui.dhall.Syntax.ExpressionScheme.{Variable, underscore}
import io.chymyst.ui.dhall.SyntaxConstants.Builtin.Natural
import io.chymyst.ui.dhall.SyntaxConstants.VarName
import io.chymyst.ui.dhall.{Parser, Semantics}
import io.chymyst.ui.dhall.SyntaxConstants.Builtin.{Bool, Natural}
import io.chymyst.ui.dhall.SyntaxConstants.{Builtin, VarName}
import io.chymyst.ui.dhall.{Parser, Semantics, TypecheckResult}
import munit.FunSuite

class SimpleSemanticsTest extends FunSuite {
Expand Down Expand Up @@ -73,4 +73,52 @@ class SimpleSemanticsTest extends FunSuite {
|in enumerate
|""".stripMargin.dhall.betaNormalized
}

test("do notation") {
val expr =
"""
|let fold
| : ∀(a : Type) →
| Optional a →
| ∀(optional : Type) →
| ∀(some : a → optional) →
| ∀(none : optional) →
| optional
| = λ(a : Type) →
| λ(o : Optional a) →
| λ(optional : Type) →
| λ(some : a → optional) →
| λ(none : optional) →
| merge { Some = some, None = none } o
|in
|
|let bind
| : ∀(a: Type) -> ∀(b: Type) -> ∀(_: Optional a) -> ∀(_: ∀(_: a) -> Optional b) -> Optional b
| = λ(a: Type)-> λ(b: Type) -> λ(x: Optional a) -> λ(f: a -> Optional b) -> fold a x (Optional b) f (None b)
|in
|
|let subtract1Optional = λ(x : Natural) → if Natural/isZero x then None Natural else Some (Natural/subtract 1 x)
|in
|
|
|let subtract3Optional = λ(x : Natural) →
| as Optional Natural in bind
| with y : Natural in subtract1Optional x
| with z : Natural in subtract1Optional y
| then subtract1Optional z
|in
|
|let _ = assert : subtract3Optional 10 === Some 7
|let _ = assert : subtract3Optional 3 === Some 0
|let _ = assert : subtract3Optional 2 === None Natural
|let _ = assert : subtract3Optional 1 === None Natural
|let _ = assert : subtract3Optional 0 === None Natural
|in
|
|[ subtract3Optional 3, subtract3Optional 2]
|""".stripMargin.dhall

expect(expr.inferType == TypecheckResult.Valid((~Builtin.List)((~Builtin.Optional)(~Natural))))
expect(expr.betaNormalized.toDhall == "[(Some 0), (None Natural)]")
}
}

0 comments on commit fb2c442

Please sign in to comment.