Ayman Bouchareb Demuirgos

General Stuff 🤹‍♀️🍲🐤🥗

This document was created back in 2020 and might not be actual nowadays. It is not supported anymore, so use thise information at your own risk.

Download WSL2 Kernel
run wsl --set-default-version 2 in windows command line, so that all future WSL machine will use WSL2.

When it comes to encoding data on the pure λ-calculus (without complex extensions such as ADTs), there are 3 widely used approaches.

The Church Encoding, which represents data structures as their folds. Using Caramel’s syntax, the natural number 3 is, for example. represented as:

0 c0 = (f x -> x)
1 c1 = (f x -> (f x))
2 c2 = (f x -&gt; (f (f x)))

	(* The syntax of our calculus. Notice that types are represented in the same way
	as terms, which is the essence of CoC. *)
	type term =
	\| Var of string
	\| Appl of term * term
	\| Binder of binder * string * term * term
	\| Star
	\| Box

	and binder = Lam \| Pi

	// Computations with extensible environment, error handling, and asynchronicity

	// I recently reviewed some F# code that turned out to be using
	//
	// Dependency Interpretation
	// https://fsharpforfunandprofit.com/posts/dependencies-4/
	//
	// and got thinking about whether one could construct a usable Zio like monad
	//
	// https://zio.dev/

	//
	// Author: Jonathan Blow
	// Version: 1
	// Date: 31 August, 2018
	//
	// This code is released under the MIT license, which you can find at
	//
	// https://opensource.org/licenses/MIT
	//
	//

	module Primes where

	open import Level using (_⊔_)
	open import Coinduction
	open import Function
	open import Data.Empty
	open import Data.Unit
	open import Data.Nat
	open import Data.Nat.Properties
	open import Data.Nat.Divisibility