Lysxia

fn main() {
  let mut q = Q(0);

  *{ println!("left" ); &mut q.0 } +=         { print!  ("right "); 1 };    // right left
   { print!  ("left "); &mut q.0 }.add_assign({ println!("right"); 1 });    // left right

  *{ print!  ("left "); &mut q   } +=         { println!("right"); Q(1) };  // left right
   { print!  ("left "); &mut q   }.add_assign({ println!("right"); Q(1) }); // left right

  ltr(0usize); // left right, even though += is used with usize: the evaluation order is determined before monomorphization

Lysxia

use bf::*;

type Program = bf![>[<[->+<]>>]<];
type Input = tape![7 7 7 7 7 7];

fn main() {
    println!("{}", Eval::<Program, Input>::default())
}

mod bf {

Lysxia

-- src/A.hs
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
module A where

import Control.Monad.Trans.State
import Data.Coerce

mapAccumLM :: forall a b c m t.
  (Traversable t, Monad m) => (b -> a -> m (c, a)) -> t b -> a -> m (t c, a)
mapAccumLM f = coerce (traverse @t @(StateT a m) @b @c) f

Lysxia

-- A fine-grained computational interpretation of Girard's intuitionistic proof-nets
-- by Delia Kesner
-- https://dl.acm.org/doi/pdf/10.1145/3498669
--
-- - Definition of the reduction relation
module CS where

open import Data.Empty
open import Data.Sum
open import Function.Base

Lysxia

module CoDebruijn where

open import Data.Product using (_×_; _,_; ∃-syntax)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

data Context : Set where
  O : Context
  1+_ : Context → Context

data Singleton : Context → Set where

Lysxia

#!/usr/bin/env cabal
{- cabal:
build-depends:
  base,
  generic-data
-}

{-# LANGUAGE ScopedTypeVariables, TypeApplications, DeriveGeneric, FlexibleContexts, UndecidableInstances, ConstraintKinds, DerivingVia #-}

import GHC.Generics (Rep, Generic)

Lysxia

-- Algebraic effects using threads

{-# LANGUAGE BlockArguments, GADTs, RankNTypes, EmptyCase, LambdaCase #-}
import Control.Concurrent
import Control.Applicative
import Control.Monad

-- Free monad as a threaded computation
-- The `forall` guarantees that `Return` can't be emitted in the middle of
-- a computation, only at the end, in a wrapper defined by `interpret`.

Lysxia

(* The SC monad (a hybrid of continuation and selection monads), monad laws, and a monad morphism from S (the selection monad) *)

Set Implicit Arguments.
Set Maximal Implicit Insertion.
Set Strict Implicit.

Record SC (s a : Type) := MkSC {
  runS : (a -> s) -> a;
  runC : (a -> s) -> s }.

Lysxia

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}

Lysxia

{-# LANGUAGE
  AllowAmbiguousTypes,
  DeriveGeneric,
  EmptyCase,
  TypeOperators,
  FlexibleInstances,
  FlexibleContexts,
  MultiParamTypeClasses,
  PolyKinds,
  TypeApplications,