This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* See https://www.johndcook.com/blog/2022/10/10/mcnugget-monoid/ *) | |
(* Stage 1 - provide mask *) | |
let rec make_mask = function | |
| 0 -> [] | |
| 1 -> [ true ] | |
| i -> false :: make_mask (i - 1) | |
let rec mix_masks l1 l2 = |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
open FStar.Pervasives.Native | |
type vec a : nat -> Type = | |
| NilV : vec a 0 | |
| ConsV : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1) | |
type response a s = | |
| Ok : bool -> a -> s -> response a s |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// See https://stackoverflow.com/questions/2565097/higher-kinded-types-with-c | |
template<typename a, typename b> | |
using Function = b (*)(const a &); | |
template<template<typename> class m> | |
struct Functor { | |
template<typename a, typename b> | |
static m<b> map(const m<a> &, Function<a, b>); | |
}; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
suspend fun doSomething(webView: WebView): Int { | |
val v1 = firstAction() | |
val v2 = secondAction(webView) | |
val v3 = thirdAction() | |
return v1 + v2 + v3 // .i.e. 42 | |
} | |
suspend fun firstAction(): Int = | |
// Do some stuff on the network for example ... |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Inspired by https://gist.github.com/tanmatra/3c2cec5d5d4345bea7a5f7c105af7238 | |
import Effects.Companion.withEffects | |
import io.smallibs.utils.Await | |
import kotlinx.coroutines.GlobalScope | |
import kotlinx.coroutines.Job | |
import kotlinx.coroutines.launch | |
import kotlin.coroutines.Continuation | |
import kotlin.coroutines.resume | |
import kotlin.coroutines.suspendCoroutine |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- | |
-- Inspired by a blog post written by Arnaud Bailly | |
-- https://abailly.github.io/posts/dependently-typed-date.html | |
-- | |
{-# OPTIONS --without-K --safe #-} | |
module Date where | |
open import Data.Nat using (ℕ; zero; suc; _≡ᵇ_; _<_; _≤_; z≤n; s≤s; _≤?_; _<?_) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// HKT simulation | |
interface Kind<out F, out A> | |
// ---------------------------------------------------------------------------- | |
interface Monad<F> { | |
fun <A, B> map(ma: Kind<F, A>, f: (A) -> B): Kind<F, B> | |
fun <A> join(ma: Kind<F, Kind<F, A>>): Kind<F, A> | |
fun <A, B> bind(ma: Kind<F, A>, f: (A) -> Kind<F, B>): Kind<F, B> = join(map(ma, f)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
object Saga { | |
type Rollback[A] = A => Any | |
case class Compensate[A](future: Future[(A, Rollback[A])]) { | |
def flatMap[B](nextCompensate: A => Compensate[B]): Compensate[B] = { | |
Compensate(future.flatMap({ | |
case (v, rollback) => | |
nextCompensate(v).future recoverWith { e => | |
rollback(v) | |
Future.failed(e) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
package control | |
trait Applicative[M[_]] extends Functor[M] { | |
def pure[A](a: A): M[A] | |
def applicative[A, B](f: M[A => B])(a: M[A]): M[B] | |
override def map[A, B](f: A => B)(a: M[A]): M[B] = applicative(pure(f))(a) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#![allow(dead_code)] | |
use std::io::{self, Read}; | |
use std::marker::PhantomData; | |
pub trait Foo<T: Read> { | |
fn get_mut(&self) -> &mut T; | |
} | |
struct FooStruct<T,R> where T:Read, R:Foo<T> { |
NewerOlder