siraben

Require Import List.
Import ListNotations.

(** A semigroup consists of an total associative operation. **)
Inductive semigroup (A : Type) (Op : A -> A -> A) : Prop :=
| semigroup_intro :
    (forall (a b c : A), Op a (Op b c) = Op (Op a b) c) -> semigroup A Op.

(** Proof that lists with append form a semigroup. **)
Theorem list_semigroup :

siraben

import Control.Monad

-- Replace T and S with any types that have monad instances.
type T a = [a]
type S a = Maybe a

-- But you must provide the l function (with the following type) to
-- make the rest of the code work.
l :: T (S a) -> S (T a)
l x = etaS (do {Just v <- x; return v})

siraben

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}

data Term
  = Con Integer
  | Div Term Term
  deriving (Show, Eq)

data Exc e a

siraben

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveFunctor #-}

module ALaCarte where
import qualified Prelude (getChar, getLine, putChar, readFile, writeFile)
import Prelude hiding (getChar, getLine, putChar, readFile, writeFile)

siraben

{-# LANGUAGE FlexibleContexts #-}

--  Karplus-Strong using infinite lists
import Control.Monad
import Data.Array.IO
import Data.List
import Foreign.C.Types
import System.Environment
import System.Exit
import System.IO

siraben

------------------------------------------------------------------------
-- A mini Haskell compiler with typeclasses.
-- Originally written by Ben Lynn, modified by Ben Siraphob
------------------------------------------------------------------------
{-
Ideas for improvements (listed rough order of difficulty for each
section)

C runtime
=========

siraben

{-# LANGUAGE TupleSections #-}
{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

-- A-Normalization, based on Matt Might's blog post:
-- http://matt.might.net/articles/a-normalization/
import Control.Monad.Cont
import Control.Monad.State
import Data.Function

siraben

{-# LANGUAGE OverloadedStrings #-}
import Data.Function
import Data.List hiding (delete)
import Data.Set
import qualified Data.Text as T

data Direction = U | R | D | L deriving (Show, Read)
type Wire = [Move]
type Pos = (Int, Int)
data Move = Move Direction Int deriving (Show, Read)

siraben

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE OverloadedLists #-}
-- Friday, April 10, 2020 at 17:25
-- Algebra of Programming in Haskell, an attempt.

-- Unlike other approaches, we will not use polytyping, which requires
-- elaborate use of generics, type families, functional dependencies,
-- and more.  Thus, we will be able to reason equationally about our

siraben

;; Virtual machine that runs SKI combinators

(subroutine $)
(subroutine arg)
(subroutine num)
(subroutine lazy)
(subroutine $arg)
(subroutine run)
(subroutine init)
(subroutine sp!)