Skip to content

Commit

Permalink
fixing compile
Browse files Browse the repository at this point in the history
  • Loading branch information
winitzki committed Nov 22, 2024
1 parent cb53fa9 commit cc43445
Show file tree
Hide file tree
Showing 2 changed files with 34 additions and 12 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -50,28 +50,44 @@ class SymbolicGraphTest extends FunSuite {
}

test("working example 2") {
sealed trait GraphExpr[+F[_]]
sealed trait GraphExpr[+F[+_]]

object GraphExpr {
final case class Rule[A, F[_]](id: A, rule: () => GraphExpr[F]) extends GraphExpr[Nothing]
final case class Rule[+A, +F[+_]](id: A, rule: () => GraphExpr[F]) extends GraphExpr[F]

final case class Wrap[F[_]] (wrap: F[GraphExpr[F]]) extends GraphExpr[F[_]]
final case class Wrap[+F[+_]](wrap: F[GraphExpr[F]]) extends GraphExpr[F]
}

import GraphExpr._

def rule[F[_]](x : => GraphExpr[F])(implicit valName: Name): Rule[String, F] = Rule[String](id = valName.value, rule = () => x)
def rule[F[+_]](x: => GraphExpr[F])(implicit valName: Name): Rule[String, F] =
Rule[String, F](id = valName.value, rule = () => x)

sealed trait Example
sealed trait ExampleF[+A]

object Example {
type F[A] = (A, Int)???
object ExampleF {
final case class Lit(s: String) extends ExampleF[Nothing]

final case class Lit(s: String) extends Example
final case class ~(l: GraphExpr[F], r : GraphExpr[F]) extends Example
final case class !(e: GraphExpr[F]) extends Example
}
final case class And[+A](l: A, r: A) extends ExampleF[A]

final case class Or[+A](l: A, r: A) extends ExampleF[A]

final case class Not[+A](x: A) extends ExampleF[A]
}
import ExampleF._

def a: Rule[String, ExampleF] = rule (Wrap (And(
Wrap (Lit("x")),
Wrap (And(
a,
b)))))

def b: Rule[String, ExampleF] = rule(
Wrap (Or(
b,
Wrap[ExampleF](And(
Wrap[ExampleF](Not(Wrap[ExampleF](Lit("y")))),
a)))))
}

}
8 changes: 7 additions & 1 deletion tutorial/programming_dhall.md
Original file line number Diff line number Diff line change
Expand Up @@ -4811,7 +4811,7 @@ let size : ∀(F : Type → Type → Type) → ∀(a : Type) → ∀(sizeF : ∀
ca Natural (sizeF a)
```

Turning now to the `depth` function, we proceed similarly and realize that the only difference is in the `sizeF` function.
Turning now to the depth calculation, we proceed similarly and realize that the only difference is in the `sizeF` function.
Instead of `sizeF` described above, we need `depthF` with the same type signature `∀(b : Type) → F b Natural → Natural`.
For the depth calculation, `depthF` should return 1 plus the maximum of all values of type `Natural` that are present. If no such values are present, it just
returns 1.
Expand All @@ -4831,6 +4831,10 @@ let depthF : ∀(a : Type) → < Leaf : a | Branch : { left : Natural, right: Na
)
```

TODO finish the code for depth and run both size and depth on an example tree

TODO express this via Traversable instances for F, use F {} Natural -> Natural as type signature

### Example: implementing "fmap"

A type constructor `F` is a **covariant functor** if it admits an `fmap` method with the type signature:
Expand Down Expand Up @@ -8454,6 +8458,8 @@ let bizip_FC

TODO run this on some examples

TODO Show that bizip_FC can be implemented in 2 different ways for FList, corresponding to the ordinary zip and to the padding zip.

## Traversable functors

## Monads and their combinators
Expand Down

0 comments on commit cc43445

Please sign in to comment.