Skip to content

Instantly share code, notes, and snippets.

Zeit Raffer zraffer

  • Ukraine
Block or report user

Report or block zraffer

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@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 ℓ₀)
View Hurkens.agda
{-# OPTIONS --type-in-type #-}
module Hurkens where
-----------------------
O = Set
Bottom : O
Bottom = (A : O) A
@zraffer
zraffer / CAT.scala
Created Nov 6, 2016
sample of abuse of Java/Scala type system for simulate given formal system
View CAT.scala
package cat
object CAT {
// system traits
sealed trait Type[Self <: Type[Self]]
sealed trait Of[Self <: Of[Self, T], T <: Type[T]]
// types
case class Ob()
@zraffer
zraffer / CCC.scala
Created Nov 4, 2016
Scala Types are objects of Cartesian Closed Category
View CCC.scala
// Scala Types are objects of Cartesian Closed Category
// (w/o equalities, probably not a category, sorry)
object CCC {
// category structure
def id[T0]: T0=>T0 = x0=>x0
def mul[T1, T2, T3](f23: T2=>T3, f12: T1=>T2): (T1=>T3) = x1 => f23(f12(x1))
// terminal object; adjunction;
type _1_ = Unit
You can’t perform that action at this time.