rntz

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
module IncrementalStreams where

import Prelude hiding (init)
import Data.Foldable (toList)
import qualified Data.Set as Set
import Data.Set (Set)
import qualified Data.Map as Map
import Data.Map (Map)

rntz

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
module IncrementalStreams where

import Prelude hiding (init)
import qualified Data.Set as Set
import Data.Set (Set)
import qualified Data.Map as Map
import Data.Map (Map)

rntz

record Preorder (A : Set) : Set1 where
  _≤_   : A → A → Set
  refl  : {a} → a ≤ a
  trans : {a b c} → a ≤ b → b ≤ c → a ≤ c

record is-lub {A} (P : Preorder A) {I} (a : I → A) (⋁a : A) : Set where
  bound : (i : I) → a i ≤ ⋁a
  least : (b : A) → ((i : I) → a i ≤ b) → ⋁a ≤ b

module _ {A B} (P : Preorder A) (Q : Preorder B) (f : A → B) where

rntz

-- A simply-typed lambda calculus, and a definition of normalisation by
-- evaluation for it.
--
-- The NBE implementation is based on a presentation by Sam Lindley from 2016:
-- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
--
-- Adapted to handle terms with explicitly typed contexts (Sam's slides only
-- consider open terms with the environments left implicit/untyped). This was a
-- pain in the ass to figure out.

rntz

/* Examples of ways in which 'void' is not a unit type in C: */

void baz(void p) {              /* error: argument may not have 'void' type */
    return p;                   /* error: void function 'baz' should not return a value [-Wreturn-type] */
}

struct foo {
    void field;                 /* error: field has incomplete type 'void' */
};

rntz

data Regex = Class [Char]   -- character class
           | Seq [Regex]    -- sequence, ABC
           | Choice [Regex] -- choice, A|B|C
           | Star Regex     -- zero or more, A*
             deriving (Show)

-- The language of a regex is, in theory, defined inductively as follows, substituting
-- lists for mathematical sets.
naive :: Regex -> [String]
naive (Class chars) = [[c] | c <- chars]

rntz

-- THIS CODE IS COMPLETELY WRONG

import qualified Data.List as List

data Regex = Class [Char]   -- character class
           | Seq [Regex]    -- sequence, ABC
           | Choice [Regex] -- choice, A|B|C
           | Star Regex     -- zero or more, A*
             deriving (Show)

rntz

{-# LANGUAGE GADTs, TypeFamilies #-}
data Type a where
  TNat :: Type Int
  TFun :: Type a -> Type b -> Type (a -> b)

type Var a = (Type a, String)
data Expr a where
  ENat :: Int -> Expr Int
  EVar :: Var a -> Expr a
  ELam :: Var a -> Expr b -> Expr (a -> b)

rntz

open import Level
-- "Wok" stands for "weak omega kategory".
mutual
  record Wok {i} (Obj : Set i) : Set (suc i) where
    coinductive
    constructor Wok:
    infix  1 Hom
    infixr 9 compo
    field Arr : (a b : Obj) -> Set i
    field Hom : (a b : Obj) -> Wok (Arr a b)

rntz

We want to maintain the sequence of iterations of some function f,

f: I × S → S

I: “input” from external world - list of edges, for example S: “state” of iteration, needs an initial value - a frontier, for example

iterate : I × S → Stream S iterate (input, state) = state :: iterate (input, f (input, state))