Roland Kuhn rkuhn

To install in Vivaldi, open the Extensions page, enable developer mode, and then drag & drop the file into the page.

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

	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,

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

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

	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

	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

	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;

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

	import scala.annotation.unchecked.uncheckedVariance

	object Trial2712 {
	trait NotUsed
	import language.higherKinds

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