rkuhn

use super::{
    handler::{self, IntoHandler, Request, Response},
    RequestReceived, StreamingResponseConfig,
};
use crate::Codec;
use futures::channel::mpsc;
use libp2p::{
    core::connection::ConnectionId,
    swarm::{NetworkBehaviour, NetworkBehaviourAction, NotifyHandler, PollParameters},
    PeerId,

rkuhn

pub fn merge_sort<T: Ord>(a: &mut [T]) {
    let len = a.len();
    if len < 2 { return }
    
    let mid = len / 2;
    {
        let (left, right) = a.split_at_mut(mid);
        merge_sort(left);
        merge_sort(right);
    }

rkuhn

struct X<T>(T);
impl<T> X<T> {
    pub fn new(t: T) -> Self {
        Self(t)
    }
    pub fn map<U>(&self, mut f: impl FnMut(&T) -> U + 'static) -> X<U> {
        X(f(&self.0))
    }
}

rkuhn

module Main

%default total

data Event = Started Int | Stopped Int | Completed Int
data State = Idle | Running | Finished

data S : s -> Type

data Activity : Type -> Event -> Type -> Type where

rkuhn

Rolands-MBP:idris-test rkuhn$ idris test.idr -o test
idris: Can't happen pickAlt - impossible case found
CallStack (from HasCallStack):
  error, called at src/IRTS/LangOpts.hs:248:25 in idris-1.3.2-9ZZwhBKx1W3Fg3FkIorcnE:IRTS.LangOpts

rkuhn

// ==UserScript==
// @name         forbid rebinding my keys
// @namespace    http://tampermonkey.net/
// @version      0.1
// @description  Get off my lawn!
// @author       Roland Kuhn
// @include      *
// @grant        none
// ==/UserScript==

rkuhn

package com.rolandkuhn.rs;

import java.net.InetSocketAddress;
import java.net.SocketAddress;
import java.util.concurrent.Executors;
import java.util.concurrent.TimeUnit;

import io.reactivesocket.ReactiveSocket;
import io.reactivesocket.client.KeepAliveProvider;
import io.reactivesocket.client.ReactiveSocketClient;

rkuhn

package akka.typed

import scala.concurrent.duration._
import org.coroutines._

object Coroutines {
  /**
   * This will be a collection of all the management commands that are sent
   * to a Session-hosting Actor via its main channel (i.e. the ActorRef that
   * is returned directly for it).

rkuhn

Some limits of equational reasoning

This is a follow-up on a discussion on gitter I had with Rob Norris. Gitter is great, but it is easier to make a coherent argument in a gist.

The monad laws allow us to assert that in the following the two results will describe computations that eventually yield the same value:

val fut1 = Future(<comp1>)
val fut2 = Future()

rkuhn

import scala.annotation.unchecked.uncheckedVariance

object Trial2712 {
  trait NotUsed
  import language.higherKinds

  /*
   * The following are simplified versions of FlowOps / FlowOpsMat and their
   * concrete subtypes.
   */