Piyush Purang ppurang

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

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

	trait Semigroup[A] {
	def op(a1: A, a2: A): A
	}

	trait Monoid[A] extends Semigroup[A] {
	def id: A
	}

	object Monoid {
	implicit def ListMonoid[A]: Monoid[List[A]] =

	import language.experimental.{ macros => scalaMacros }
	import reflect.macros.Context

	package object macros {
	def safe[A](expr: A) = macro safeImpl[A]

	def safeImpl[A](c: Context)(expr: c.Expr[A]): c.Expr[A] = {
	import c.universe._

	def isIgnoredStatement(tree: Tree) = tree match {

	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])

	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] = ???
	}

	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

	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._



	{-
	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:

	#!/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