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 β„“β‚€)