Skip to content

Instantly share code, notes, and snippets.

Avatar
🚀
let it be

Bay Raktar zraffer

🚀
let it be
View GitHub Profile
View file.idr
Id0 : (0 A : Type) -> Type
Id0 a = () -> a
Id1 : (1 A : Type) -> Type
Id1 a = a
@zraffer
zraffer / encodings.md
Created May 19, 2020 — forked from zmactep/encodings.md
Number encodings
View encodings.md

Alternative to the Church, Scott and Parigot encodings of data on the Lambda Calculus.

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

Church Encoding

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 -> (f (f x)))
@zraffer
zraffer / test.agda
Created Dec 17, 2019
agda editor highlight
View test.agda
{-# OPTIONS --type-in-type #-}
{- remark -}
module _ where
record Go (A : Set) : Set where
constructor Go!
field go : (a : A) A Set
field og : A -> forall (a : A) -> Set
open Go {{...}} public
@zraffer
zraffer / truffle-material.md
Created Apr 20, 2018 — forked from smarr/truffle-material.md
Truffle: Languages and Material
View truffle-material.md
View LinVect.scala
object LinVect {
type K = Double
// type Nat
trait NatClass[N] {
val nat: Int
}
View LinVect.scala
object LinVect {
type K = Double
trait NAT[N] { val nat: Int }
def NAT[N: NAT]: NAT[N] = implicitly
def nat[N: NAT]: Int = NAT[N].nat
trait NAT_10
implicit object NAT_10 extends NAT[NAT_10]
View LinVect.scala
object LinVect {
type K = Double
trait NAT[N] { val nat: Int }
def NAT[N: NAT]: NAT[N] = implicitly
def nat[N: NAT]: Int = NAT[N].nat
trait NAT_10
implicit object NAT_10 extends NAT[NAT_10]
@zraffer
zraffer / Main.scala
Created Dec 10, 2017
scala-bimodule
View Main.scala
object Main {
abstract class Ab[A] {
val add: (A, A) => A
val neg: A => A
}
abstract class Ring[R] extends Ab[R] {
val mul: (R, R) => R
}
abstract class Field[F] extends Ring[F] {
@zraffer
zraffer / README.md
Last active Oct 13, 2017
implicit issue
View README.md

error for line 9 in check-minimal.agda

Failed to solve the following constraints:
  lsuc (_ℓ₀_52 ℓ₂) ⊔ (lsuc (_ℓ₁_53 ℓ₂) ⊔ lsuc (lsuc ℓ₂))
  = lsuc (_ℓ₀_52 ℓ₂) ⊔
    (lsuc (_ℓ₁_53 ℓ₂) ⊔ (lsuc (lsuc ℓ₂) ⊔ (lsuc .ℓ₁ ⊔ .ℓ₀)))
  lsuc .ℓ₁ ⊔ .ℓ₀ = _ℓ₀_52 ℓ₂ ⊔ lsuc (_ℓ₁_53 ℓ₂)
  _47 := λ {ℓ₀} {ℓ₁} ℓ₂ P₀ → P₀ → Set ℓ₁ [blocked on problem 26]
 [26] _P₀_41 ℓ₂ =< Set ℓ₀ : Set (lsuc ℓ₀)