xuwei-k

import scala.quoted.*

object SummonDebugMacro {
  inline def summonDebug[A]: A = ${summonDebugImpl[A]}

  def summonDebugImpl[A: Type](using q: Quotes): Expr[A] = {
    import q.reflect.*
    Expr.summon[A] match {
      case Some(tree) =>
        println(tree.show)

AndrasKovacs

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.