Skip to content

Instantly share code, notes, and snippets.

View bblfish's full-sized avatar

Henry Story bblfish

194 followers · 52 following
View GitHub Profile
@bblfish
bblfish / VerifiableCredentials.fix1.jsonld
Created February 1, 2023 10:02
Fix for VerifiableCredentials example 1
{
"@context": [
"https://www.w3.org/2018/credentials/v1",
"https://www.w3.org/2018/credentials/examples/v1"
],
"id": "http://example.edu/credentials/1872",
"type": ["VerifiableCredential", "AlumniCredential"],
"issuer": "https://example.edu/issuers/565049",
"issuanceDate": "2010-01-01T19:23:24Z",
"credentialSubject": {
@bblfish
bblfish / VerifiableCredential.jsonld
Last active February 1, 2023 10:10
Example1 Verifiable Credential
{
"@context": [
"https://www.w3.org/2018/credentials/v1",
"https://www.w3.org/2018/credentials/examples/v1"
],
"id": "http://example.edu/credentials/1872",
"type": ["VerifiableCredential", "AlumniCredential"],
"issuer": "https://example.edu/issuers/565049",
"issuanceDate": "2010-01-01T19:23:24Z",
"credentialSubject": {
@bblfish
bblfish / ActorK.scala
Created September 5, 2022 07:34 — forked from Swoorup/ActorK.scala
Typed Actors using Cats Effect, FS2 and Deferred Magic
import cats.effect.syntax.all.*
import cats.syntax.all.*
import cats.effect.*
import fs2.Stream
import cats.effect.std.Queue
import scala.concurrent.duration.*
import lib.FSM
import lib.actor.{Actor, AskMsg}
@bblfish
bblfish / basic-http-model.agda
Created July 8, 2022 06:54
Very basic model of an interpretation of http header to show that it is a dependent type
{-# OPTIONS --without-K --safe #-}
Type = Set
record Σ {A : Type } (B : A → Type) : Type where
constructor
_,_
field
pr₁ : A
pr₂ : B pr₁
@bblfish
bblfish / Paths.scala
Last active October 24, 2021 09:38
How does creating files and dirs change mod times
import java.io.{File, FileOutputStream, IOException}
import java.nio.file.*
import java.nio.file.attribute.*
import scala.collection.immutable.Map
trait Cache(var db: Map[Path, BasicFileAttributes]):
lazy val mod: Map[Path, FileTime] = db.view.mapValues(_.lastModifiedTime).toMap
val start = java.nio.file.Path.of(".")
@bblfish
bblfish / ServerOpticsTest.scala
Last active July 10, 2021 17:23
package monocle
import monocle.Lens
import monocle.syntax.all.*
import java.time.{Clock, Instant}
import scala.collection.immutable.*
//for an intro to Monocle see the video https://twitter.com/bblfish/status/1413758476896153601
// and the thread of references above it.
@bblfish
bblfish / MessageSignaturev04_ApendixB22_Test.sc
Created April 27, 2021 14:44
Test Example from Message Signature Spec
import java.nio.charset.StandardCharsets
import java.security.spec.{PKCS8EncodedKeySpec, X509EncodedKeySpec}
import java.security.KeyFactory
import java.util.Base64
val singleSlsh = raw"\\\n *".r
//java.security.Security.addProvider(new org.bouncycastle.jce.provider.BouncyCastleProvider)
def rfc8792single(str: String) = singleSlsh.replaceAllIn(str.stripMargin,"")
def base64Decode(str: String) = Base64.getDecoder.decode(str)
@bblfish
bblfish / Adjunctions2-3Quiver.cql
Created November 18, 2020 08:16
Calculate Sigma, Delta, Pi for a functor from 2 to 3 arrow quivers on a very simple instance
// This calculates the Sigma, Delta, Pi adjunctions for a functor F from
// the schema for 2 arrow quivers to 3 arrow quivers on a simple instance
// see https://www.categoricaldata.net/ .
// ie it shows two translations of a directed graph to a RDF like directed
// graph. Sigma just gives each arrow a type, Pi duplicates the graph as
// many times as their are nodes and for all the arrows in one of the duplicated
// graphs assigns it one of the nodes.
typeside Ty = literal {
java_types
@bblfish
bblfish / Prefix.scala
Created August 24, 2020 21:14
Dotty inheritance of path dependent types
package org.w3.banana
import scala.util._
trait Prefix[T <: RDFObj](using val rdf: T) {
def prefixName: String
def prefixIri: String
def apply(value: String): rdf.URI
def unapply(iri: rdf.URI): Option[String]
@bblfish
bblfish / PointedGraph.scala
Created August 24, 2020 15:44
Trying to get the types in dotty to line up.
package org.w3.banana
import org.w3.banana._
trait RDFOps[Rdf <: RDF & Singleton](using val Rdf: RDF) {
def emptyGraph: Rdf.Graph
}
trait PointedGraph[Rdf <: RDF & Singleton](using val ops: RDFOps[Rdf]) {