d-plaindoux

import TList.{TCons, TNil}

import scala.annotation.targetName

enum TList[A]:
  case TNil[A]() extends TList[A]
  case TCons[A, X <: A, T <: TList[A]](x: X, t: T) extends TList[A]

sealed trait Elem[A, X, XS <: TList[A]]:
  def get(l: XS): X

d-plaindoux

import :=:.Refl
import Type.*
import TypeRepr.*

import scala.annotation.tailrec

enum :=:[A, B]:
  case Refl[E]() extends :=:[E, E]

enum Type:

d-plaindoux

(* 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 =

d-plaindoux

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

d-plaindoux

// 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>);
};

d-plaindoux

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 ...

d-plaindoux

// 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

d-plaindoux

--
-- 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; _≤?_; _<?_)

d-plaindoux

// 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))

d-plaindoux

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)