myuon

theory CR
imports "~~/src/HOL/Nominal/Nominal"
begin

atom_decl var

nominal_datatype lambda =
  Var var
| App lambda lambda (infixl "$" 120)
| Abs "«var»lambda" ("lam [_]._" [100,100] 100)

myuon

theory Adc2017
imports Main
begin

section {* States *}

type_synonym id = string
type_synonym state = "id ⇒ nat"

definition empty :: "state" where

myuon

~$ cabal sandbox init
Writing a default package environment file to
/home/ioijoi/program/widx/cabal.sandbox.config
Creating a new sandbox at /home/ioijoi/program/widx/.cabal-sandbox
~$ cabal install --only-dependencies && cabal new-build
Resolving dependencies...
Notice: installing into a sandbox located at
/home/ioijoi/program/widx/.cabal-sandbox
Configuring cabal-doctest-1.0.2...
Configuring call-stack-0.1.0...

myuon

#!/usr/bin/env stack
{- stack
  runghc
  --package extensible
  --package lens
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

myuon

#!/usr/bin/env stack

newtype Machine i o = Machine { runMachine :: i -> IO (o, Machine i o) }

fibM :: Machine () Int
fibM = go 1 1 where
  go :: Int -> Int -> Machine () Int
  go i j = Machine $ \() -> do
    putStrLn $ "machineA: " ++ show (i,j)
    return $ (,) (i+j) $ go j (i+j)

myuon

-- example from: https://arxiv.org/abs/1611.09259

interface Send X = send : X -> Unit
interface Recieve X = recieve : X
interface Abort = aborting : Zero

catter : [Receive (List X)]List X
catter! = on receive! { nil -> nil | xs -> append xs catter! }

pipe : <Send X>Unit -> <Receive X>Y -> [Abort]Y

myuon

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
import Control.Monad
import Control.Applicative
import Control.Monad.Skeleton
import qualified Data.Map as M
import Text.Trifecta

myuon

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
import Control.Object
import Control.Monad.State.Strict
import Control.Monad.Skeleton
import Data.Functor.Identity
import Data.Functor.Sum

myuon

{-# LANGUAGE GADTs #-}
import Control.Monad
import Data.Functor.Identity
import Linear.V2
import Pipes
import Pipes.Core
import SDLight.Types

(&&&) :: Monad m => Pipe a b m () -> Pipe a' b' m () -> Pipe (a,a') (b,b') m ()
p1 &&& p2 = do

myuon

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}

import Data.Tagged
import GHC.TypeLits

-- standard list datatype
data List = N | C Int List

-- tagless final list