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.

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)

WesleyAC

#!/usr/bin/env bash

cd $(dirname $0)

docker run --rm -it -v "$(pwd)":/home/rust/src -v cargo-git:/home/rust/.cargo/git -v cargo-registry:/home/rust/.cargo/registry -v "$(pwd)/target/":/home/rust/src/target ekidd/rust-musl-builder:nightly-2021-01-01 sudo chown -R rust:rust /home/rust/.cargo/git /home/rust/.cargo/registry /home/rust/src/target

docker run --rm -it -v "$(pwd)":/home/rust/src -v cargo-git:/home/rust/.cargo/git -v cargo-registry:/home/rust/.cargo/registry -v "$(pwd)/target/":/home/rust/src/target ekidd/rust-musl-builder:nightly-2021-01-01 cargo build --release

AndrasKovacs

{-
Inductive-recursive universes, indexed by levels which are below an arbitrary type-theoretic ordinal number (see HoTT book 10.3). This includes all kinds of transfinite levels as well.

Checked with: Agda 2.6.1, stdlib 1.3

My original motivation was to give inductive-recursive (or equivalently: large inductive)
semantics to to Jon Sterling's cumulative algebraic TT paper:

Hakky54

Keytool CheatSheet 🔐

Some history

This cheat sheet came into life when I started working on a tutorial of setting up one way tls and two way tls, which can be found here: GitHub - Mutual TLS SSL

Creation and importing

Generate a Java keystore and key pair

keytool -genkeypair -keyalg RSA -keysize 2048 -keystore keystore.jks -alias server -validity 3650

iravid

import $ivy.`dev.zio::zio:1.0.0-RC8-12`
import $ivy.`dev.zio::zio-streams:1.0.0-RC8-12`

import zio._, zio.stream._

object Step1 {
  import java.nio.file.{Files, Paths, Path}
  import scala.collection.JavaConverters._
  import zio.blocking._

erdeszt

trait Coercible[A, B] {
  def coerce(a: A): B
}

def coerce[A, B](a: A)(implicit coerceAB: Coercible[A, B]): B = {
  coerceAB.coerce(a)
}

trait Newtype[+T] {
  val value: T

travisbrown

class Nil
class Cons[X, Xs]

class First[List] { type X }
object First {
  type Aux[List, X0] = First[List] { type X = X0 }

  implicit val nilFirst: Aux[Nil, Nil] = ???
  implicit def consFirst[X0, Xs]: Aux[Cons[X0, Xs], X0] = ???
}

OlivierBlanvillain

Revisiting Tagless Final Interpreters

Tageless Final interpreters are an alternative to the traditional Algebraic Data Type (and generalized ADT) based implementation of the interpreter pattern. This document presents the Tageless Final approach with Scala, and shows how Dotty with it's recently added implicits functions makes the approach even more appealing. All examples are direct translations of their Haskell version presented in the Typed Tagless Final Interpreters: Lecture Notes (section 2).

The interpreter pattern has recently received a lot of attention in the Scala community. A lot of efforts have been invested in trying to address the biggest shortcomings of ADT/GADT based solutions: extensibility. One can first look at cats' Inject typeclass for an implementation of [Data Type à la Carte](http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesA

tonymorris

package com.nicta
package rng

import scalaz._, Scalaz._, effect._

// A data type representing a person.
// We are going to produce random instances.
// Note that this data type is recursive.
// The `children` field holds 0 or many Person instances.
case class Person(name: String, age: Int, surname: Option[String], children: List[Person])