Elvecent

module Universal where

open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open Relation.Binary.PropositionalEquality.≡-Reasoning
open import Agda.Primitive
open import Data.Nat hiding (_⊔_)
open import Data.Unit hiding (setoid)
open import Data.Bool
open import Data.Nat.Properties

Elvecent

data List {α} : Set α → Set α where
  [] : ∀ {X} → List X
  _::_ : ∀ {X} → X → List X → List X

map : ∀ {α β} → {A : Set α} → {B : Set β} →
      (f : A → B) → List A → List B
map f [] = []
map f (x :: xs) = f x :: map f xs

data hList {α} : List (Set α) → Set α where

Elvecent

Module ClassicLogic.
  Definition LEM := forall A : Prop, A \/ ~A.
  Definition CONTRA := forall A B : Prop, (~A -> ~B) -> (B -> A).

  Axiom lem : LEM.
  Axiom contra : CONTRA.

  Notation "( x , y , .. , z )" := (conj .. (conj x y) .. z) (at level 0).
End ClassicLogic.

Elvecent

Require Import Coq.Lists.List.
Import ListNotations.

Inductive hlist : list Type -> Type :=
| nil : hlist []
| cons {Ts : list Type}
       {T : Type} : T -> hlist Ts -> hlist (T :: Ts).

Notation "[ ]" := nil (format "[ ]") : hlist_scope.
Notation "[ x ]" := (cons x nil) : hlist_scope.

Elvecent

{-# Language TypeSynonymInstances
, FlexibleInstances
, MultiParamTypeClasses
, KindSignatures
, GADTs
, DataKinds
, TypeFamilies
, AllowAmbiguousTypes
, TypeApplications
#-}

Elvecent

{-# Language GADTs,
DataKinds,
KindSignatures,
StandaloneDeriving,
DeriveFunctor,
TypeFamilies
#-}

import Data.Function

Elvecent

{-# Language DeriveFunctor #-}

module Parser where

newtype Parser a = Parser { parse :: String -> [(a, String)] }
  deriving Functor

parserBind :: Parser a -> (a -> Parser b) -> Parser b
parserBind (Parser p) mf = Parser $ \s ->
  p s >>= (\(x,s) -> parse (mf x) s)

Elvecent

-- packages "free" and "transformers" assumed

{-# LANGUAGE DeriveFunctor #-}

module Main where

import Control.Monad.Trans.Free
import Control.Monad.Trans.Class

data CoroutineF a = Yield a 

Elvecent

module Utils.Concurrent (mkPipeline, launchNukes) where

import           Control.Concurrent       (threadDelay)
import           Control.Concurrent.Async (Async, async, cancel, wait)
import           Control.Concurrent.STM   (TBQueue, atomically, newTBQueueIO,
                                           readTBQueue, writeTBQueue)
import           Control.Monad            (forever, void)
import           Control.Monad.IO.Class   (MonadIO, liftIO)
import           GHC.Natural              (Natural)

Elvecent

The purpose of this text is to guide a reader through the first step towards grokking continuations as presented in Haskell (callCC not covered). The reader is assumed to have basic knowledge of Haskell including some understanding of monads.

Abstracting away computations

Suppose we are given a list of lists of integers and we want to compute the sum of squares of products of those lists. This task naturally breaks down into three steps:

1. Take product of each list of integers and thus form a new list of integers.
2. In that list, square every integer, again forming a new list of integers.
3. Summate the resulting list.

But to produce this algorithm we need to parse the whole problem and revert it (i. e. start with the last step): the problem's descriptions starts with "sum" and the corresponding algorithm starts with "product". Does it really need to be like this?