Skip to content

Instantly share code, notes, and snippets.

View zraffer's full-sized avatar
🚀
let it be

Bay Raktar zraffer

🚀
let it be
16 followers · 18 following
  • Ukraine
View GitHub Profile
@zraffer
zraffer / file.idr
Created June 22, 2020 14:06
Id0 : (0 A : Type) -> Type
Id0 a = () -> a
Id1 : (1 A : Type) -> Type
Id1 a = a
@zraffer
zraffer / encodings.md
Created May 19, 2020 14:22 — forked from zmactep/encodings.md
Number encodings

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 December 17, 2019 17:44
agda editor highlight
{-# 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 / Screenshot.png
Last active July 25, 2019 16:48
Screenshot.png
@zraffer
zraffer / truffle-material.md
Created April 20, 2018 17:14 — forked from smarr/truffle-material.md
Truffle: Languages and Material
@zraffer
zraffer / LinVect.scala
Created January 5, 2018 18:55
object LinVect {
type K = Double
// type Nat
trait NatClass[N] {
val nat: Int
}
@zraffer
zraffer / LinVect.scala
Created December 28, 2017 10:55
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 / LinVect.scala
Created December 27, 2017 17:17
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 December 10, 2017 18:52
scala-bimodule
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 October 13, 2017 15:11
implicit issue

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 ℓ₀)