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

/* 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

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))

rntz

I shoved this into a git repo, https://github.com/rntz/talon-tutoring-resources

rntz

chart
(A,A') -> (B,B')

lens
get : A -> B
put : A × B' -> A'

chart
get : A -> B
weird : A × A' -> B'