hanshoglund

- Write an interactive explorer for (potentially) infinite data structures.
- Several data structures can be supported, start with:
  - Lists: `[Word8]`
  - Rose trees: `Tree Word8`
- The application should present a terminal interface with the following interaction:
  - Program status up
  - A random infinite value of the data structure type (chosen at compile type) is generated
  - The following loop is executed until the user presses 'q' or Ctrl-D
    - A *subset* of the data structure is displayed, including one focused element which is highlighted
    - The user presses one of the keys h j k or l to move focus

hanshoglund

## Monad transformers and orphans
- Orphan instances are generally distrusted in Haskell and for good reason: they break module composition.
  - As a minimal example, if module A defines class C and module B defines type T, we generally want to put an instance (C T) in A or B.
  - If we allow it in other modules, imagine it is defined in modules X and Y: now X and Y *cannot* be imported by the same module.

- However there is a problem with (monad) transformers.
  - Transformers require an exponential number of instances. For example say we have two effect types and corresponding transformers.
    For simplcitity we will put all classes and types in separate modules. 
    - `MonadFoo` (declared in `A`)
    - `MonadBar` (in `B`)

hanshoglund

hanshoglund

t, u, v for kind (*->*)->(*->*), f, g, h for kind (* -> *), a, b, c for kind *

hanshoglund

https://eprint.iacr.org/2017/872.pdf
http://ieeexplore.ieee.org/document/4031371/?part=1

hanshoglund

Given a basic typed lambda calculus E

  E := x | E E | \x:T -> E
     | Succ E | Z
     | (E, E) | E.fst | E.snd
     | True | False | if E then E else E

and a base boolean language B
  
  B :=

hanshoglund

  , "Int"               `isSubtypeOf`         "forall a.a"

  , "{foo:Int}"         `isSubtypeOf`         "forall r.(r\\foo) => {foo:Int|r}"
  , "{foo:Int,bar:Int}" `isSubtypeOf`         "forall r.(r\\foo) => {foo:Int|r}"
  , "{foo:Int,bar:Int}" `isNotSubtypeOf`      "{foo:Int}"

  , "{foo:Int} -> <L:Int>"
    `isSubtypeOf`
    "forall a r r1. (r\\foo, r1\\L) => {foo : a | r} -> <L : a | r1>"

hanshoglund

\f a -> (f a) 
  :: (a -> b) -> a -> b
\f a b -> (f a >>= ($ b))
  :: Monad m => (a -> m (b -> m c)) -> a -> b -> m c
\f a b c -> (f a >>= ($ b) >>= ($ c))
  :: Monad m => (a -> m (b -> m (c -> m d))) -> a -> b -> c -> m d

hanshoglund

F E C G
(related, Jupiter: F E C D)

And that's how we'll begin the *Wizard and I*
I haven't *missed him so far*
Puerto Rico, you *lovely island*
Assassins (almost): In the *U.S.A.* you can *work your way*
Aladdin: I can *show you a world*

hanshoglund

-- Row-type records as variants and variants as records

-- type Either a b = (left :: a | right :: b)
type Either a b = 
  forall r . { left :: a -> r, right :: b -> r} -> r

-- type Pair a b = forall r . (fst :: a->r | snd :: b->r) -> r
type PairHelper a b = 
  forall r . { fst :: a -> r, snd :: b -> r } -> r
type Pair a b =