text:
![LiquidHaskell](/resources/logo.png)

[![Hackage](https://img.shields.io/hackage/v/liquidhaskell.svg)](https://hackage.haskell.org/package/liquidhaskell) [![Hackage-Deps](https://img.shields.io/hackage-deps/v/liquidhaskell.svg)](http://packdeps.haskellers.com/feed?needle=liquidhaskell) [![Build Status](https://img.shields.io/circleci/project/ucsd-progsys/liquidhaskell/master.svg)](https://circleci.com/gh/ucsd-progsys/liquidhaskell)
[![Windows build status](https://ci.appveyor.com/api/projects/status/78y7uusjcgor5p16/branch/develop?svg=true)](https://ci.appveyor.com/project/varosi/liquidhaskell-nlhra/branch/develop)

Main Web site
-------------

* [Try LiquidHaskell in your browser](http://goto.ucsd.edu:8090/index.html)
* [Splash page with examples and link to blog](https://ucsd-progsys.github.io/liquidhaskell-blog/)
* [120 minute workshop with more examples](http://ucsd-progsys.github.io/lh-workshop/01-index.html)
* [Long ish Tutorial](http://ucsd-progsys.github.io/liquidhaskell-tutorial/)

Questions
-----------
If you have any questions

* Join the Liquid Haskell [slack channel](https://join.slack.com/t/liquidhaskell/shared_invite/enQtMjY4MTk3NDkwODE3LTY1YzBiY2JlZjBjMTM5M2ZkMjNmZDk5ZjA2MGQyZjQ5ZjBmYjZjNGMzOTUyMTU2MDlmM2YzZDM2YjhiMWFjM2I)
* Mail the [users mailing list](https://groups.google.com/forum/#!forum/liquidhaskell)
* Create a github issue

Contributing Guide
------------------

Please see the [contributing guide](CONTRIBUTING.md)

Requirements
------------

LiquidHaskell requires (in addition to the cabal dependencies)

- SMTLIB2 compatible solver installed and its executable found on PATH

How To Clone, Build and Install
-------------------------------

You may want to [try LiquidHaskell online](http://goto.ucsd.edu:8090/index.html)

See [install instructions](INSTALL.md)

How To Run
----------

To verify a file called `foo.hs` at type

    $ liquid foo.hs

How to Run inside GHCi
----------------------

To run inside `ghci` e.g. when developing do:

    $ stack ghci liquidhaskell
    ghci> :m +Language.Haskell.Liquid.Liquid
    ghci> liquid ["tests/pos/Abs.hs"]

See [this file](NIX.md) for instructions on running inside a custom `nix`-shell.

How To Get Editor Support
-------------------------

To get Liquid Haskell in your editor use the Haskell IDE Engine and activate the liquid plugin.
For example,

- [VS Code](https://code.visualstudio.com/)

    1. Install the [haskell-ide-engine](https://github.com/haskell/haskell-ide-engine)
    2. Enable Haskell Language Server extension from VS Code.
    3. In the VS Code settings search for `liquid` and enable the `Liquid On` extension.

How To Run Regression Tests
---------------------------

You can run all the tests by

    $ stack test

To pass in specific parameters and run a subset of the tests

    $ stack test liquidhaskell --fast  --test-arguments "--liquid-opts --no-termination -p Unit"

Or your favorite number of threads, depending on cores etc.

You can directly extend and run the tests by modifying

    tests/test.hs

How to Profile
--------------

1. Build with profiling on

    ```
    $ stack build liquidhaskell --fast --profile
    ```

2. Run with profiling

    ```
    $ stack exec -- liquid range.hs +RTS -hc -p
    $ stack exec -- liquid range.hs +RTS -hy -p
    ```

    Followed by this which shows the stats file

    ```
    $ more liquid.prof
    ```

    or by this to see the graph

    ```
    $ hp2ps -e8in -c liquid.hp
    $ gv liquid.ps
    ```

    etc.

How to Get Stack Traces On Exceptions
-------------------------------------

1. Build with profiling on

    ```
    $ stack build liquidhaskell --fast --profile
    ```

2. Run with backtraces

    ```
    $ liquid +RTS -xc -RTS foo.hs
    ```

    ```
    stack exec -- liquid List00.hs +RTS -p -xc -RTS
    ```

Working With Submodules
-----------------------

 - To update the `liquid-fixpoint` submodule, run

    ```
    cd ./liquid-fixpoint
    git fetch --all
    git checkout <remote>/<branch>
    cd ..
    ```

   This will update `liquid-fixpoint` to the latest version on `<branch>`
   (usually `master`) from `<remote>` (usually `origin`).

 - After updating `liquid-fixpoint`, make sure to include this change in a
   commit! Running

    ```
    git add ./liquid-fixpoint
    ```

   will save the current commit hash of `liquid-fixpoint` in your next commit
   to the `liquidhaskell` repository.

 - For the best experience, **don't** make changes directly to the
   `./liquid-fixpoint` submodule, or else git may get confused. Do any
   `liquid-fixpoint` development inside a separate clone/copy elsewhere.

 - If something goes wrong, run

    ```
    rm -r ./liquid-fixpoint
    git submodule update --init
    ```

   to blow away your copy of the `liquid-fixpoint` submodule and revert to the
   last saved commit hash.

 - Want to work fully offline? git lets you add a local directory as a remote.
   Run

    ```
    cd ./liquid-fixpoint
    git remote add local /path/to/your/fixpoint/clone
    cd ..
    ```

   Then to update the submodule from your local clone, you can run

    ```
    cd ./liquid-fixpoint
    git fetch local
    git checkout local/<branch>
    cd ..
    ```

Command Line Options
====================

LiquidHaskell supports several command line options, to configure the
checking. Each option can be passed in at the command line, or directly
added to the source file via:

```haskell
    {-@ LIQUID "option-within-quotes" @-}
```

for example, to disable termination checking (see below)

```haskell
    {-@ LIQUID "--no-termination" @-}
```

You may also put command line options in the environment variable
`LIQUIDHASKELL_OPTS`. For example, if you add the line:

```
    LIQUIDHASKELL_OPTS="--diff"
```

to your `.bashrc` then, by default, all files will be
*incrementally checked* unless you run with the overriding
`--full` flag (see below).

Theorem Proving
---------------

To enable theorem proving, e.g. as [described here](https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html)
use the option

```haskell
    {-@ LIQUID "--reflection" @-}
```

To additionally turn on _proof by logical evaluation_ use the option

```haskell
    {-@ LIQUID "--ple" @-}
```

You can see many examples of proofs by logical evaluation in `benchmarks/popl18/ple/pos`

This flag is **global** and will symbolically evaluate all the terms that appear in the specifications.

As an alternative, the `liquidinstanceslocal` flag has local behavior. [See](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/benchmarks/proofautomation/pos/Unification.hs)

```
{-@ LIQUID "--ple-local" @-}
```

will only evaluate terms appearing in the specifications
of the function `theorem`, in the function `theorem` is
annotated for automatic instantiation using the following
liquid annotation

```
{-@ automatic-instances theorem @-}
```

Incremental Checking
--------------------

LiquidHaskell supports *incremental* checking where each run only checks
the part of the program that has been modified since the previous run.

```
    $ liquid --diff foo.hs
```

Each run of `liquid` saves the file to a `.bak` file and the *subsequent* run

    + does a `diff` to see what has changed w.r.t. the `.bak` file
    + only generates constraints for the `[CoreBind]` corresponding to the
       changed top-level binders and their transitive dependencies.

The time savings are quite significant. For example:

```
    $ time liquid --notermination -i . Data/ByteString.hs > log 2>&1

    real	7m3.179s
    user	4m18.628s
    sys	    0m21.549s
```

Now if you go and tweak the definition of `spanEnd` on line 1192 and re-run:

```
    $ time liquid -d --notermination -i . Data/ByteString.hs > log 2>&1

    real	0m11.584s
    user	0m6.008s
    sys	    0m0.696s
```

The diff is only performed against **code**, i.e. if you only change
specifications, qualifiers, measures, etc. `liquid -d` will not perform
any checks. In this case, you may specify individual definitions to verify:

```
    $ liquid -b bar -b baz foo.hs
```

This will verify `bar` and `baz`, as well as any functions they use.

If you always want to run a given file with diff-checking, add
the pragma:

    {-@ LIQUID "--diff" @-}

Full Checking (DEFAULT)
-----------------------

To force LiquidHaskell to check the **whole** file (DEFAULT), use:

    $ liquid --full foo.hs

to the file. This will override any other `--diff` incantation
elsewhere (e.g. inside the file.)

If you always want to run a given file with full-checking, add
the pragma:

    {-@ LIQUID "--full" @-}

Specifying Different SMT Solvers
--------------------------------

By default, LiquidHaskell uses the SMTLIB2 interface for Z3.

To run a different solver (supporting SMTLIB2) do:

    $ liquid --smtsolver=NAME foo.hs

Currently, LiquidHaskell supports

+ [CVC4](http://cvc4.cs.stanford.edu/web/)
+ [MathSat](http://mathsat.fbk.eu/download.html )

To use these solvers, you must install the corresponding binaries
from the above web-pages into your `PATH`.

You can also build and link against the Z3 API (faster but requires more
dependencies). If you do so, you can use that interface with:

    $ liquid --smtsolver=z3mem foo.hs

Short Error Messages
--------------------

By default, subtyping error messages will contain the inferred type, the
expected type -- which is **not** a super-type, hence the error -- and a
context containing relevant variables and their type to help you understand
the error. If you don't want the above and instead, want only the
**source position** of the error use:

    --short-errors

Short (Unqualified) Module Names
-------------------------------

By default, the inferred types will have fully qualified module names.
To use unqualified names, much easier to read, use:

    --short-names

Disabling Checks on Functions
-----------------------------

You can _disable_ checking of a particular function (e.g. because it is unsafe,
or somehow not currently outside the scope of LH) by using the `ignore` directive.

For example,

```haskell
{-@ ignore foo @-}
```

will _disable_ the checking of the code for the top-level binder `foo`.

See `tests/pos/Ignores.hs` for an example.

Totality Check
--------------

LiquidHaskell proves the absence of pattern match failures.

For example, the definition

    fromJust :: Maybe a -> a
    fromJust (Just a) = a

is not total and it will create an error message.
If we exclude `Nothing` from its domain, for example using the following specification

    {-@ fromJust :: {v:Maybe a | (isJust v)} -> a @-}

`fromJust` will be safe.

Use the `no-totality` flag to disable totality checking.

    liquid --no-totality test.hs

Termination Check
-----------------

By **default** a termination check is performed on all recursive functions.

Use the `--no-termination` option to disable the check

    liquid --no-termination test.hs

In recursive functions the *first* algebraic or integer argument should be decreasing.

The default decreasing measure for lists is length and Integers its value.

### Default Termination Metrics

The user can specify the *size* of a data-type in the data definition

```haskell
    {-@ data L [llen] a = Nil | Cons { x::a, xs:: L a} @-}
```

In the above, the measure `llen`, which needs to be defined by the user
(see below), is defined as the *default metric* for the type `L a`. LH
will use this default metric to _automatically_ prove that the following
terminates:

```haskell
    append :: L a -> L a -> L a
    append N           ys = ys
    append (Cons x xs) ys = Cons x (append xs ys)
```

as, by default the *first* (non-function) argument with an
associated size metric is checked to be strictly terminating
and non-negative at each recursive call.

A default termination metric is a Haskell function that is proved terminating
using structural induction. To deactivate structional induction check on the
termination metric, use the `--trust-sizes` flag.

### Explicit Termination Metrics

However, consider the function `reverse`

```haskell
    reverseAcc :: L a -> L a -> L a
    reverseAcc acc N           = acc
    reverseAcc acc (Cons x xs) = reverseAcc (Cons x acc) xs
```

Here, the first argument does not decrease, instead
the second does. We can tell LH to use the second
argument using the *explicit termination metric*

```haskell
    reverseAcc :: L a -> xs:L a -> L a / [llen xs]
```

which tells LH that the `llen` of the second argument `xs`
is what decreases at each recursive call.

Decreasing expressions can be arbitrary refinement expressions, e.g.,

```haskell
    {-@ merge :: Ord a => xs:L a -> ys:L a -> L a / [llen xs + llen ys] @-}
```

states that at each recursive call of `merge` the _sum of the lengths_
of its arguments will decrease.

### Lexicographic Termination Metrics

Some functions do not decrease on a single argument, but rather a
combination of arguments, e.g. the Ackermann function.

```haskell
    {-@ ack :: m:Int -> n:Int -> Nat / [m, n] @-}
    ack m n
      | m == 0          = n + 1
      | m > 0 && n == 0 = ack (m-1) 1
      | m > 0 && n >  0 = ack (m-1) (ack m (n-1))
```

In all but one recursive call `m` decreases, in the final call `m`
does not decrease but `n` does. We can capture this notion of `m`
normally decreases, but if it does not, `n` will decrease with a
*lexicographic* termination metric `[m, n]`.

An alternative way to express this specification is by annotating
the function's type with the appropriate *numeric* decreasing expressions.
As an example, you can give `ack` a type

    {-@ ack :: m:Nat -> n:Nat -> Nat / [m,n] @-}

stating that the *numeric* expressions `[m, n]` are lexicographically decreasing.

### Mutually Recursive Functions

When dealing with mutually recursive functions you may run into a
situation where the decreasing parameter must be measured *across* a
series of invocations, e.g.

```haskell
    even :: Int -> Bool
    even 0 = True
    even n = odd (n-1)

    odd :: Int -> Bool
    odd  n = not (even n)
```

In this case, you can introduce a ghost parameter that *orders the functions*

```haskell
    {-@ isEven :: n:Nat -> z:{v:Int | v = 0} -> Bool / [n, z] @-}
    isEven :: Int -> Int -> Bool
    isEven 0 _ = True
    isEven n _ = isOdd (n-1) 1

    {-@ isOdd :: n:Nat -> z:{v:Int | v = 1} -> Bool / [n, z] @-}
    isOdd :: Int -> Int -> Bool
    isOdd  n _ = not (isEven n 0)
```

thus recovering a decreasing measure for the pair of functions, the
pair of arguments. This can be encoded with the lexicographic
termination annotation as shown above.
See [tests/pos/mutrec.hs](tests/pos/mutrec.hs) for the full example.

### Automatic Termination Metrics

Apart from specifying a specific decreasing measure for
an Algebraic Data Type, the user can specify that the ADT
follows the expected decreasing measure by

```haskell
    {-@ autosize L @-}
```

Then, LH will define an instance of the function `autosize`
for `L` that decreases by 1 at each recursive call and use
`autosize` at functions that recurse on `L`.

For example, `autosize L` will refine the data constructors
of `L a` with the `autosize :: a -> Int` information, such
that

```haskell
    Nil  :: {v:L a | autosize v = 0}
    Cons :: x:a -> xs:L a -> {v:L a | autosize v = 1 + autosize xs}
```

Also, an invariant that `autosize` is non negative will be generated

```haskell
    invariant  {v:L a| autosize v >= 0 }
```

This information is all LiquidHaskell needs to prove termination
on functions that recurse on `L a` (on ADTs in general.)

### Disabling Termination Checking

To *disable* termination checking for `foo` that is,
to *assume* that it is terminating (possibly for some
complicated reason currently beyond the scope of LH)
you can write

```haskell
    {-@ lazy foo @-}
```

Total Haskell
--------------

LiquidHaskell provides a total Haskell flag that checks both totallity and termination of the program,
overriding a potential no-termination flag.

    liquid --total-Haskell test.hs

Lazy Variables
--------------

A variable can be specified as `LAZYVAR`

    {-@ LAZYVAR z @-}

With this annotation the definition of `z` will be checked at the points where
it is used. For example, with the above annotation the following code is SAFE:

    foo   = if x > 0 then z else x
      where
        z = 42 `safeDiv` x
        x = choose 0

By default, all the variables starting with `fail` are marked as LAZY, to defer
failing checks at the point where these variables are used.

No measure fields
------------------

When a data type is refined, Liquid Haskell automatically turns the data constructor fields into measures.
For example,

    {-@ data L a = N | C {hd :: a, tl :: L a} @-}

will automatically create two measures `hd` and `td`.
To deactivate this automatic measure definition, and speed up verification, you can use the `no-measure-fields` flag.

    liquid --no-measure-fields test.hs

Prune Unsorted Predicates
--------------------------

The `--prune-unsorted` flag is needed when using *measures over specialized instances* of ADTs.

For example, consider a measure over lists of integers

```haskell
    sum :: [Int] -> Int
    sum [] = 0
    sum (x:xs) = 1 + sum xs
```

This measure will translate into strengthening the types of list constructors

```
    [] :: {v:[Int] | sum v = 0 }
    (:) :: x:Int -> xs:[Int] -> {v:[Int] | sum v = x + sum xs}
```

But what if our list is polymorphic `[a]` and later instantiate to list of ints?
The workaround we have right now is to strengthen the polymorphic list with the
`sum` information

```
    [] :: {v:[a] | sum v = 0 }
    (:) :: x:a -> xs:[a] -> {v:[a] | sum v = x + sum xs}
```

But for non numeric `a`s, refinements like `x + sum xs` are ill-sorted!

We use the flag `--prune-unsorted` to prune away unsorted expressions
(like `x + sum xs`) inside refinements.

```
    liquid --prune-unsorted test.hs
```

Case Expansion
-------------------------

By default LiquidHaskell expands all data constructors to the case statements.
For example,
if `F = A1 | A2 | .. | A10`,
then LiquidHaskell will expand the code
`case f of {A1 -> True; _ -> False}`
to `case f of {A1 -> True; A2 -> False; ...; A10 -> False}`.
This expansion can lead to more precise code analysis
but it can get really expensive due to code explosion.
The `no-case-expand` flag prevents this expansion and keeps the user
provided cases for the case expression.

    liquid --no-case-expand test.hs

Higher order logic
-------------------
The flag `--higherorder` allows reasoning about higher order functions.

Restriction to Linear Arithmetic
---------------------------------
When using `z3` as the solver, LiquidHaskell allows for non-linear arithmetic:
division and multiplication on integers are interpreted by `z3`. To treat division
and multiplication as uninterpreted functions use the `linear` flag

    liquid --linear test.hs

Counter examples (Experimental!)
--------------------------------
When given the `--counter-examples` flag, LiquidHaskell will attempt to produce
counter-examples for the type errors it discovers. For example, see
[tests/neg/ListElem.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/neg/ListElem.hs)

```
% liquid --counter-examples tests/neg/ListElem.hs

...

tests/neg/ListElem.hs:12:1-8: Error: Liquid Type Mismatch

 12 | listElem _ []      = False
      ^^^^^^^^

   Inferred type
     VV : {VV : Bool | VV == True}
     VV = True

   not a subtype of Required type
     VV : {VV : Bool | Prop VV <=> Set_mem ?b (listElts ?a)}

   In Context
     ?a : {?a : [a] | len ?a >= 0}
     ?a = [1]

     ?b : a
     ?b = 0
```

The `--counter-examples` flag requires that each type in the context be
an instance of `GHC.Generics.Generic` or `Test.Targetable.Targetable`
(provided as part of LiquidHaskell).  LiquidHaskell cannot generate
counter-examples for polymorphic types, but will try (naively) to
instantiate type variables with `Int` (as seen in the example above).

Writing Specifications
======================

Modules WITHOUT code
--------------------

When checking a file `target.hs`, you can specify an _include_ directory by

    liquid -i /path/to/include/  target.hs

Now, to write specifications for some **external module** `Foo.Bar.Baz` for which
you **do not have the code**, you can create a `.spec` file at:

    /path/to/include/Foo/Bar/Baz.spec

See, for example, the contents of

+ [include/Prelude.spec](https://github.com/ucsd-progsys/liquidhaskell/blob/master/include/Prelude.spec)
+ [include/Data/List.spec](https://github.com/ucsd-progsys/liquidhaskell/blob/master/include/Data/List.spec)
+ [include/Data/Vector.spec](https://github.com/ucsd-progsys/liquidhaskell/blob/master/include/Data/Vector.spec)

**Note**:

+ The above directories are part of the LH prelude, and included by
  default when running `liquid`.
+ The `.spec` mechanism is *only for external modules** without code,
  see below for standalone specifications for **internal** or **home** modules.

Modules WITH code: Data
-----------------------

Write the specification directly into the .hs or .lhs file,
above the data definition. See, for example, [tests/pos/Map.hs](tests/pos/Map.hs)

    {-@
    data Map k a <l :: k -> k -> Prop, r :: k -> k -> Prop>
      = Tip
      | Bin (sz    :: Size)
            (key   :: k)
            (value :: a)
            (left  :: Map <l, r> (k <l key>) a)
            (right :: Map <l, r> (k <r key>) a)
    @-}
    data Map k a = Tip
                 | Bin Size k a (Map k a) (Map k a)

You can also write invariants for data type definitions
together with the types. For example, see [tests/pos/record0.hs](tests/pos/record0.hs)

    {-@ data LL a = BXYZ { size  :: {v: Int | v > 0 }
                         , elems :: {v: [a] | (len v) = size }
                         }
    @-}

Finally you can specify the variance of type variables for data types.
For example, see [tests/pos/Variance.hs](tests/pos/Variance.hs), where data type `Foo` has four
type variables `a`, `b`, `c`, `d`, specified as invariant, bivariant,
covariant and contravariant, respectively.

    data Foo a b c d
    {-@ data variance Foo invariant bivariant covariant contravariant @-}

Modules WITH code: Functions
----------------------------

Write the specification directly into the .hs or .lhs file,
above the function definition. [For example](tests/pos/spec0.hs)

    {-@ incr :: x:{v: Int | v > 0} -> {v: Int | v > x} @-}
    incr   :: Int -> Int
    incr x = x + 1

Modules WITH code: Type Classes
-------------------------------

Write the specification directly into the .hs or .lhs file,
above the type class definition. [For example](tests/pos/Class.hs)

    {-@ class Sized s where
          size :: forall a. x:s a -> {v:Int | v = (size x)}
    @-}
    class Sized s where
      size :: s a -> Int

Any measures used in the refined class definition will need to be
*generic* (see [Specifying Measures](#specifying-measures)).

As an alternative, you can refine class instances.
[For example](tests/classes/pos/Inst00.hs)

~~~~
instance Compare Int where

{-@ instance Compare Int where
    cmax :: Odd -> Odd -> Odd
  @-}

cmax y x = if x >= y then x else y
~~~~

When `cmax` method is used on `Int`, liquidHaskell will give it
the refined type `Odd -> Odd -> Odd`.

Note that currently liquidHaskell does not allow refining instances of
refined classes.

Modules WITH code: QuasiQuotation
---------------------------------

Instead of writing both a Haskell type signature *and* a
LiquidHaskell specification for a function, the `lq`
quasiquoter in the `LiquidHaskell` module can be used
to generate both from just the LiquidHaskell specification.

```haskell
module Nats (nats) where

{-@ nats :: [{v:Int | 0 <= v}] @-}
nats :: [Int]
nats = [1,2,3]
```

can be written as

```haskell
{-# LANGUAGE QuasiQuotes #-}
module Nats (nats) where

import LiquidHaskell

[lq| nats :: [{v:Int | 0 <= v}] |]
nats = [1,2,3]
```

and the `lq` quasiquoter will generate the plain `nats :: [Int]` when GHC
compiles the module.

Refined type aliases (see the next section) can also be written inside `lq`; for
example:

```haskell
{-# LANGUAGE QuasiQuoters #-}
module Nats (Nat, nats) where

[lq| type Nat = {v:Int | 0 <= v} |]

[lq| nats :: [Nat] |]
nats = [1,2,3]
```

Here, the `lq` quasiquoter will generate a plain Haskell
type synonym for `Nat` as well as the refined one.

Note that this is still an experimental feature, and
currently requires that one depend on LiquidHaskell
as a build dependency for your project; the quasiquoter
will be split out eventually into an independent,
dependency-light package. Also, at this time, writing
a type inside `lq` which refers to a refined type alias
for which there is not a plain Haskell type synonym of the
same name will result in a "not in scope" error from GHC.

Standalone Specifications for Internal Modules
----------------------------------------------

Recall that the `.spec` mechanism is only for modules whose
code is absent; if code is present then there can be multiple,
possibly conflicting specifications. Nevertheless, you may want,
for one reason or another, to write (assumed) specifications
outside the file implementing the module.

You can do this as follows.

`Lib.hs`

```haskell
module Lib (foo) where

foo a = a
```

now, instead of a `.spec` file, just use a haskell module, e.g. `LibSpec.hs`

```haskell
module LibSpec ( module Lib ) where

import Lib

-- Don't forget to qualify the name!

{-@ Lib.foo :: {v:a | false} -> a @-}
```

and then here's `Client.hs`

```haskell
module Client where

import Lib      -- use this if you DON'T want the spec
import LibSpec  -- use this if you DO want the spec, in addition to OR instead of the previous import.

bar = foo 1     -- if you `import LibSpec` then this call is rejected by LH
```

Inductive Predicates
--------------------

**Very Experimental**

LH recently added support for *Inductive Predicates*
in the style of Isabelle, Coq etc. These are encoded
simply as plain Haskell GADTs but suitably refined.

Apologies for the minimal documentation; see the
following examples for details:

* [Even and Odd](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/ple/pos/IndEven.hs)
* [Permutations](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/ple/pos/IndPerm.hs)
* [Transitive Closure](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/ple/pos/IndStar.hs)
* [RegExp Derivatives](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/ple/pos/RegexpDerivative.hs)
* [Type Safety of STLC](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/ple/pos/STLC2.hs)

Implicit Arguments
------------------

**Experimental**

There is experimental support for implicit arguments, solved for with congruence closure. For example, consider [Implicit1.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/pos/Implicit1.hs):

```haskell
{-@ type IntN N = {v:Int | v = N} @-}

{-@ foo :: n:Int ~> (() -> IntN n) -> IntN {n+1} @-}
foo f = 1 + f ()

{-@ test1 :: IntN 11 @-}
test1 = foo (\_ -> 10)
```

Here, the refinement on `(\_ -> 10) :: Int -> { v:Int | v = 10 }` allows us to solve for `n = 10`, the implicit argument to `foo`.

Refinement Type Aliases
-----------------------

#### Predicate Aliases

Often, the propositions in the refinements can get rather long and
verbose. You can write predicate aliases like so:

    {-@ predicate Lt X Y = X < Y        @-}
    {-@ predicate Ge X Y = not (Lt X Y) @-}

and then use the aliases inside refinements, [for example](tests/pos/pred.hs)

    {-@ incr :: x:{v:Int | (Pos v)} -> { v:Int | ((Pos v) && (Ge v x))} @-}
    incr :: Int -> Int
    incr x = x + 1

See [Data.Map](benchmarks/esop2013-submission/Base.hs) for a more substantial
and compelling example.

**Syntax:** The key requirements for type aliases are:

- Value parameters are specified in **upper**case: `X`, `Y`, `Z` etc.

#### Class Laws

Class laws can be defined and checked using the `class laws`
and `instance laws` keywords. For an example, see:

* [class-laws/pos/SemiGroup.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/06d22aa070933d9ea833e30d84ed91de2a28eaee/tests/class-laws/pos/SemiGroup.hs)
* [class-laws/pos/SemiGroup.hs](tests/class-laws/pos/SemiGroup.hs)

#### Type Aliases

Similarly, it is often quite tedious to keep writing

    {v: Int | v > 0}

Thus, LiquidHaskell supports refinement-type aliases of the form:

    {-@ type Gt      N = {v: Int | N <  v} @-}
    {-@ type GeNum a N = {v: a   | N <= v} @-}

or

    {-@ type SortedList a = [a]<{\fld v -> (v >= fld)}> @-}

or

    {-@ type OMap k a = Map <{\root v -> v < root}, {\root v -> v > root}> k a @-}

or

    {-@ type MinSPair a = (a, OSplay a) <\fld -> {v : Splay {v:a|v>fld} | 0=0}> @-}

and then use the above in signatures like:

    {-@ incr: x: Int -> GeNum Int x @-}

or

    {-@ incr: x: Int -> Gt x @-}

and:

    {-@ assert insert :: (Ord a) => a -> SortedList a -> SortedList a @-}

see [tests/pos/ListSort.hs](tests/pos/ListSort.hs)

and:

    {-@ assert insert :: (Ord k) => k -> a -> OMap k a -> OMap k a @-}

see [tests/pos/Map.hs](tests/pos/Map.hs)

**Syntax:** The key requirements for type aliases are:

1. Type parameters are specified in **lower**case: `a`, `b`, `c` etc.
2. Value parameters are specified in **upper**case: `X`, `Y`, `Z` etc.

Infix Logic Operators
---------------------

You can define infix operators in logic, following [Haskell's infix notation](https://www.haskell.org/onlinereport/decls.html#fixity).
For example, if `(+++)` is defined as a measure or reflected function, you can use it infix by declaring

    {-@ infixl 9 +++ @-}

Note: infix operators cannot contain the dot character `.`.

Specifying Measures
-------------------

Can be placed in .spec file or in .hs/.lhs file wrapped around `{-@ @-}`

Value measures: [include/GHC/Base.spec](include/GHC/Base.spec)

    measure len :: forall a. [a] -> GHC.Types.Int
    len ([])     = 0
    len (y:ys)   = 1 + len(ys)

Propositional measures: [tests/pos/LambdaEval.hs](tests/pos/LambdaEval.hs)

    {-@
    measure isValue      :: Expr -> Bool
    isValue (Const i)    = true
    isValue (Lam x e)    = true
    isValue (Var x)      = false
    isValue (App e1 e2)  = false
    isValue (Plus e1 e2) = false
    isValue (Fst e)      = false
    isValue (Snd e)      = false
    isValue (Pair e1 e2) = ((? (isValue(e1))) && (? (isValue(e2))))
    @-}

Raw measures: [tests/pos/meas8.hs](tests/pos/meas8.hs)

    {-@ measure rlen :: [a] -> Int
    rlen ([])   = {v | v = 0}
    rlen (y:ys) = {v | v = (1 + rlen(ys))}
    @-}

Generic measures: [tests/pos/Class.hs](tests/pos/Class.hs)

    {-@ class measure size :: a -> Int @-}
    {-@ instance measure size :: [a] -> Int
        size ([])   = 0
        size (x:xs) = 1 + (size xs)
    @-}
    {-@ instance measure size :: Tree a -> Int
        size (Leaf)       = 0
        size (Node x l r) = 1 + (size l) + (size r)
    @-}

**Note:** Measure names **do not** have to be the same as
field name, e.g. we could call the measure `sz` in the above
as shown in [tests/pos/Class2.hs](tests/pos/Class2.hs).

Haskell Functions as Measures (beta): [tests/pos/HaskellMeasure.hs](tests/pos/HaskellMeasure.hs)

Inductive Haskell Functions from Data Types to some type can be lifted to logic

```haskell
    {-@ measure llen @-}
    llen        :: [a] -> Int
    llen []     = 0
    llen (x:xs) = 1 + llen xs
```

The above definition
  - refines list's data constructors types with the llen information, and
  - specifies a singleton type for the haskell function
        `llen :: xs:[a] -> {v:Int | v == llen xs}`
    If the user specifies another type for llen, say
        `llen :: xs:[a] -> {v:Int | llen xs >= 0}`
    then the auto generated singleton type is overwritten.

Inlines
-------

The `inline`  lets you use a Haskell function in a type specification.

```
{-@ inline max @-}
{-@ max :: Int -> Int -> Int @-}
max :: Int -> Int -> Int
max x y = if x > y then x else y
```

For example, if you write the above you can then write a function:

```haskell
{-@ floor :: x:Int -> {v:Int | max 0 x} @-}
floor :: Int -> Int
floor x
  | x <= 0    = 0
  | otherwise = x
```

That is, you can use the haskell `max` in the refinement type and
it will automatically get “expanded” out to the full definition.
This makes it useful e.g. to reuse plain Haskell code to compose
specifications, and to share definitions common to refinements and code.

However, as they are *expanded* at compile time, `inline` functions
**cannot be recursive**. The can call _other_ (non-recursive) inline functions.

If you want to talk about arbitrary (recursive) functions inside your types,
then you need to use `reflect` described [in the blog] (https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html)

Self-Invariants
===============

Sometimes, we require specifications that allow *inner* components of a
type to refer to the *outer* components, typically, to measure-based
properties of outer components. For example, the following invariant
about `Maybe` values

    {-@ type IMaybe a = {v0 : Maybe {v : a | ((isJust v0) && v = (fromJust v0))} | 0 = 0 } @-}

states that the *inner* `a` enjoys the property that the *outer* container
is definitely a `Just` and furthermore, the inner value is exactly the same
as the `fromJust` property of the outer container.

As another example, suppose we have a [measure](include/Data/Set.spec):

    measure listElts :: [a] -> (Set a)
    listElts([])   = {v | (? Set_emp(v))}
    listElts(x:xs) = {v | v = Set_cup(Set_sng(x), listElts(xs)) }

Now, all lists enjoy the property

    {-@ type IList a = {v0 : List  {v : a | (Set_mem v (listElts v0)) } | true } @-}

which simply states that each *inner* element is indeed, a member of the
set of the elements belonging to the entire list.

One often needs these *circular* or *self* invariants to connect different
levels (or rather, to *reify* the connections between the two levels.) See
[this test](tests/pos/maybe4.hs) for a simple example and `hedgeUnion` and
[Data.Map.Base](benchmarks/esop2013-submission/Base.hs) for a complex one.

Abstract and Bounded Refinements
================================

This is probably the best example of the abstract refinement syntax:

+ [Abstract Refinements](tests/pos/Map.hs)
+ [Bounded Refinements](benchmarks/icfp15/pos/Overview.lhs)

Unfortunately, the best documentation for these two advanced features
is the relevant papers at

+ [ESOP 2013](https://ranjitjhala.github.io/static/abstract_refinement_types.pdf)
+ [ICFP 2015](https://arxiv.org/abs/1507.00385)

The bounds correspond to Horn implications between abstract refinements,
which, as in the classical setting, correspond to subtyping constraints
that must be satisfied by the concrete refinements used at any call-site.

Dependent Pairs
===============
Dependent Pairs are expressed by binding the initial tuples of the pair. For example
`incrPair` defines an increasing pair.

    {-@ incrPair :: Int -> (x::Int, {v:Int | x <= v}) @-}
    incrPair i = (i, i+1)

Internally dependent pairs are implemented using abstract refinement types.
That is `(x::a, {v:b | p x})` desugars to `(a,b)<\x -> {v:b | p x}>`.

Invariants
==========

LH lets you locally associate invariants with specific data types.

For example, in [tests/measure/pos/Using00.hs](tests/measure/pos/Using00.hs) every
list is treated as a Stream. To establish this local invariant one can use the
`using` declaration

    {-@ using ([a]) as  {v:[a] | (len v > 0)} @-}

denoting that each list is not empty.

Then, LiquidHaskell will prove that this invariant holds, by proving that *all
calls* to List's constructors (ie., `:` and `[]`) satisfy it, and
will assume that each list element that is created satisfies
this invariant.

With this, at the [above](tests/measure/neg/Using00.hs) test LiquidHaskell
proves that taking the `head` of a list is safe.
But, at [tests/measure/neg/Using00.hs](tests/measure/neg/Using00.hs) the usage of
`[]` falsifies this local invariant resulting in an "Invariant Check" error.

**WARNING:** There is an older _global_ invariant mechanism that
attaches a refinement to a datatype globally.
Do not use this mechanism -- it is *unsound* and about to
deprecated in favor of something that is [actually sound](https://github.com/ucsd-progsys/liquidhaskell/issues/126)

Forexample,  the length of a list cannot be negative

    {-@ invariant {v:[a] | (len v >= 0)} @-}

LiquidHaskell can prove that this invariant holds, by proving that all List's
constructors (ie., `:` and `[]`) satisfy it.(TODO!) Then, LiquidHaskell
assumes that each list element that is created satisfies
this invariant.

Formal Grammar of Refinement Predicates
=======================================

(C)onstants
-----------

    c := 0, 1, 2, ...

(V)ariables
-----------

    v := x, y, z, ...

(E)xpressions
-------------

    e := v                      -- variable
       | c                      -- constant
       | (e + e)                -- addition
       | (e - e)                -- subtraction
       | (c * e)                -- multiplication by constant
       | (v e1 e2 ... en)       -- uninterpreted function application
       | (if p then e else e)   -- if-then-else

(R)elations
-----------

    r := ==               -- equality
       | /=               -- disequality
       | >=               -- greater than or equal
       | <=               -- less than or equal
       | >                -- greater than
       | <                -- less than

(P)redicates
------------

    p := (e r e)          -- binary relation
       | (v e1 e2 ... en) -- predicate (or alias) application
       | (p && p)         -- and
       | (p || p)         -- or
       | (p => p)         -- implies
       | (not p)          -- negation
       | true
       | false

Specifying Qualifiers
=====================

There are several ways to specify qualifiers.

By Separate `.hquals` Files
---------------------------

You can write qualifier files e.g. [Prelude.hquals](include/Prelude.hquals)

If a module is called or imports

    Foo.Bar.Baz

Then the system automatically searches for

    include/Foo/Bar/Baz.hquals

By Including `.hquals` Files
----------------------------

Additional qualifiers may be used by adding lines of the form:

    {-@ include <path/to/file.hquals> @-}

to the Haskell source. See, [this](tests/pos/meas5.hs) for example.

In Haskell Source or Spec Files
-------------------------------

Finally, you can specifiers directly inside source (.hs or .lhs) or spec (.spec)
files by writing as shown [here](tests/pos/qualTest.hs)

    {-@ qualif Foo(v:Int, a: Int) : (v = a + 100)   @-}

**Note** In addition to these, LiquidHaskell scrapes qualifiers from all
the specifications you write i.e.

1. all imported type signatures,
2. measure bodies and,
3. data constructor definitions.

Generating HTML Output
======================

The system produces HTML files with colorized source, and mouseover
inferred type annotations, which are quite handy for debugging failed
verification attempts.

- **Regular Haskell** When you run: `liquid foo.hs` you get a file
  `foo.hs.html` with the annotations. The coloring is done using
  `hscolour`.

- **Markdown + Literate Haskell** You can also feed in literate haskell files
  where the comments are in [Pandoc markdown](http://johnmacfarlane.net/pandoc/demo/example9/pandocs-markdown.html).
  In this case, the tool will run `pandoc` to generate the HTML from the comments.
  Of course, this requires that you have `pandoc` installed as a binary on
  your system. If not, `hscolour` is used to render the HTML.

  It is also possible to generate *slide shows* from the above.
  See the [slides directory](docs/slides) for an example.

Editor Integration
==================

+ [Emacs/Flycheck](https://github.com/ucsd-progsys/liquid-types.el)
+ [Vim/Syntastic](https://github.com/ucsd-progsys/liquid-types.vim)

Command Line Options
====================

To see all options, run `liquid --help`. Here are some common options:

- `--cabaldir` will automatically find a .cabal file in the ancestor
  path from which the target file belongs, and then add the relevant
  source and dependencies to the paths searched for by LiquidHaskell.

  This means we don't have to manually do `-i src` etc. when checking
  large projects, which can be tedious e.g. within emacs.

- `--diff` performs differential checking, i.e. only checks those binders
  that have transitively affected by edits since the previous check.
  Can speed things up greatly during editing.

- `--short-names` prints out non-qualified names i.e. `Int` instead of
  `GHC.Types.Int` for inferred type annotations and error messages.

**Pragmas** are useful for embedding options directly within the source file,
that is, somewhere in the file (perhaps at the top) put in:

    {-@ LIQUID "--diff"        @-}
    {-@ LIQUID "--short-names" @-}
    {-@ LIQUID "--cabaldir"    @-}

to have the relevant option be used for that file.

Generating Performance Reports
------------------------------

We have set up infrastructure to generate performance reports using [Gipeda](https://github.com/nomeata/gipeda).

Gipeda will generate a static webpage that tracks the performance improvements
and regressions between commits. To generate the site, first ensure you have the
following dependencies available:

* Git
* Cabal >= 1.18
* GHC
* Make
* Bash (installed at `/bin/bash`)

After ensuring all dependencies are available, from the Liquid Haskell
directory, execute:

    cd scripts/performance
    ./deploy-gipeda.bash

This will download and install all the relevant repositories and files. Next, to
generate the performance report, use the `generate-site.bash` script. This script
has a few options:

* `-s [hash]`: Do not attempt to generate performance reports for any commit
older than the commit specified by the entered git hash
* `-e [hash]`: Do not attempt to generate performance reports for any commit
newer than the commit specified by the entered git hash
* `-f`: The default behavior of `generate-site.bash` is to first check if logs
have been created for a given hash. If logs already exist, `generate-site.bash`
will not recreate them. Specify this option to skip this check and regenerate
all logs.

You should expect this process to take a very long time. `generate-site.bash`
will compile each commit, then run the entire test suite and benchmark suite
for each commit. It is suggested to provide a manageable range to `generate-site.bash`:

    ./generate-site.bash -s [starting hash] -e [ending hash]

...will generate reports for all commits between (inclusive) [starting hash]
and [ending hash].

    ./generate-site.bash -s [starting hash]

... will generate reports for all commits newer than [starting hash]. This command
can be the basis for some automated report generation process (i.e. a cron job).

Finally, to remove the Gipeda infrastructure from your computer, you may execute:

    ./cleanup-gipeda.bash

...which will remove any files created by `deploy-gipeda.bash` and `generate-site.bash`
from your computer.

Configuration Management
------------------------

It is very important that the version of Liquid Haskell be maintained properly.

Suppose that the current version of Liquid Haskell is `A.B.C.D`:

+ After a release to hackage is made, if any of the components `B`, `C`, or `D` are missing, they shall be added and set to `0`. Then the `D` component of Liquid Haskell shall be incremented by `1`. The version of Liquid Haskell is now `A.B.C.(D + 1)`

+ The first time a new function or type is exported from Liquid Haskell, if any of the components `B`, or `C` are missing, they shall be added and set to `0`. Then the `C` component shall be incremented by `1`, and the `D` component shall stripped. The version of Liquid Haskell is now `A.B.(C + 1)`

+ The first time the signature of an exported function or type is changed, or an exported function or type is removed (this includes functions or types that Liquid Haskell re-exports from its own dependencies), if the `B` component is missing, it shall be added and set to `0`. Then the `B` component shall be incremented by `1`, and the `C` and `D` components shall be stripped. The version of Liquid Haskell is now `A.(B + 1)`

+ The `A` component shall be updated at the sole discretion of the project owners.

Updating GHC
============

Here's a script to generate the diff for the `desugar` modules.

```
export GHCSRC=$HOME/Documents/ghc

# Checkout GHC-8.2.2
(cd $GHCSRC && git checkout ghc-8.2.2 && git pull)

# make a patch
diff -ur $GHCSRC/compiler/deSugar src/Language/Haskell/Liquid/Desugar > liquid.patch

# Checkout GHC-8.4.3
(cd $GHCSRC && git checkout ghc-8.2.2 && git pull)

# Copy GHC desugarer to temporary directory
cp -r $GHCSRC/compiler/deSugar .

# Patch
(cd deSugar && patch -p5 --merge --ignore-whitespace < ../liquid.patch)

# Copy stuff over
for i in src/Language/Haskell/Liquid/Desugar/*.*; do j=$(basename $i); echo $j; cp deSugar/$j src/Language/Haskell/Liquid/Desugar; done
```

Here's the magic diff that we did at some point that we keep bumping up to new GHC versions:

https://github.com/ucsd-progsys/liquidhaskell/commit/d380018850297b8f1878c33d0e4c586a1fddc2b8#diff-3644b76a8e6b3405f5492d8194da3874R224

repository: yiyunliu/liquidhaskell

branch_name: refs/heads/develop

gha_language: Haskell

gha_license_id: NOASSERTION

repo_name: yiyunliu/liquidhaskell


text:
---
title: A tutorial on the free-energy framework for modelling perception and learning
layout: single
---

### Based on [K. Friston](http://www.fil.ion.ucl.ac.uk/~karl/A%20free%20energy%20principle%20for%20the%20brain.pdf) and following [R. Bogacz](http://www.sciencedirect.com/science/article/pii/S0022249615000759) I shortly summarise the former, and solve the programming exercises given in the paper. This motives [another post](https://tmorville.github.io/projects/active-learning), taking a more general look at active learning in ML.

---

### Why is this important/exciting?

[R. Bogacz](http://www.sciencedirect.com/science/article/pii/S0022249615000759) delivers a detailed and beautifully made tutorial on a subject that can be very difficult to understand, [Variational Bayes](https://en.wikipedia.org/wiki/Variational_Bayesian_methods), as seen from Karl Fristons perspective; Namely invoking the [Free-Energy principle](https://en.wikipedia.org/wiki/Free_energy_principle) to motivate Active Inference. In the last decade, Active Inference has gained traction with the wider neuroscientific community, and recently Karl was [measured](https://www.ucl.ac.uk/news/slms/slms-news/slms/ucl-neuroscientists-most-influential) to be the most influential neuroscientist in the modern era.

### Nomenclature:

I use the same notation as in R. Bogacz. The code implements and refers to equations in the paper, and network graphs were provided by Bogacz himself.

---

### Introduction - Biological intuition
A simple organism is trying to infer the size $$v$$ of a food item. The only source of noisy information is one photoreceptor that signals the light reflected from this item, we denote this $$u$$. The non-linear function that relates size $$v$$ to photosensory input $$u$$ is assumed to be $$g(v)=v^2$$. We assume that this signal is normally distributed with mean $$g(v)$$ and variance $$\Sigma_{v}$$.

---

### Part I - Bayes

We can write of the the likelihood function (probability of a size $$v$$ given a signal $$u$$) as

$$ p(v\vert u)=f(u;g(v),\Sigma_{u}) $$

where

$$ f(x;\mu,\Sigma)=\frac{1}{\sqrt{2\pi\Sigma}}\mbox{exp}\left(-\frac{(x-\mu)^{2}}{2\Sigma}\right) $$

is the normal distribution with mean $$\mu$$ and variance $$\Sigma$$.

Through learning or evolutionary filtering, the agent has been endowed with priors on the expected size of food items, and therefore expects sizes of food items to normally distributed with mean $$v_{p}$$ and $$\Sigma_{p}$$ where the subscript $$p$$ stands for prior. Formally

$$ p(v)=f(v;v{p},\Sigma_{p}) $$.

To compute the exact distribution of sensory input $$u$$ we can formulate the posterior using Bayes theorem

$$p(v|u)=\frac{p(v)p(u|v)}{p(u)}$$

where the denominator is

$$p(u)=\int p(v)p(u|v)dv$$

and sum the whole range of possible sizes.

The following code implements such an exact solution and plots it.

```python
import numpy as np
import seaborn as sns
import matplotlib.pyplot as plt
from scipy.stats import norm

sns.set(style="white", palette="muted", color_codes=True)

%matplotlib inline
```

```python
# non-linear transformation of size to perceived sensory input e.g. g(phi)
def sensory_transform(input):

    sensory_output = np.square(input)

    return sensory_output
```

The reason we explicitly define $$g(\cdot)$$ is that we might want to change it later. For now we assume a simple non-linear relation $$g(v)=v^2$$. The following snippet of code assumes values of $$v,\Sigma_u,v_p,\Sigma_p$$ and plots the posterior distribution.

```python
def exact_bayes():

    # variabels
    v = 2 # real size of item
    sigma_u = 1 # standard deviation of noisy input
    v_p = 3 # mean of prior
    sigma_p = 1 # variance of prior / sensory noise
    s_range = np.arange(0.01,5,0.01) # range of sensory input
    s_step = 0.01 # step size

    # exact bayes (equation 4)
    numerator = (np.multiply(norm.pdf(s_range,v_p,sigma_p),# prior
                            norm.pdf(v,sensory_transform(s_range),sigma_u))) # likelihood
    normalisation = np.sum(numerator*s_step) # denominator / model evidence / p(noisy input) (equation 5)
    posterior = numerator / normalisation # posterior

    # plot exact bayes
    plt.figure(figsize=(7.5,2.5))
    plt.plot(s_range,posterior)
    plt.ylabel(r' $p(v | u)$')
    sns.despine()
```

```python
exact_bayes()
```

![png]({{ site.url }}{{ site.baseurl }}/assets/images/Bogacz_5_0.png)

Inspecting the graph, we find that approximately $$\phi=1.6$$ maximises the posterior. There are two fundamental problems with this approach

 1. The posterior does not take a standard form, and is thus described by (potentially) infinitely many moments, instead of just simple sufficient statistics, such as the mean and the variance of a gaussian.

 2. The normalisation term that sits in the numerator of Bayes formula

$$
p(u)=\int p(v)p(u|v)dv
$$

can be complicated and numerical solutions often rely on computationally intense algorithms, such as the [Expectation-Maximisation algorithm](https://en.wikipedia.org/wiki/Expectation%E2%80%93maximization_algorithm).

### Part II - Iteration using Eulers method

We are interested in a more general way of finding the value that maximises the posterior $$ \phi $$. This involves maximising the numerator of Bayes equation. As this is independent of the denominator and therefore maximising $$p(v)p(u\vert v)$$ will maximise the posterior. By taking the logarithm to the numerator we get

$$
F=\mbox{ln}p(\phi)+\mbox{ln}p(u|\phi)
$$

and the dynamics can be derived (see notes) to be

$$
\dot{\phi}=\frac{v_{p}-\phi}{\Sigma_{p}}+\frac{u-g(\phi)}{\Sigma_{u}}g^{'}(\phi)
$$

The next snippit of code asumes values for $$v,\sigma_u,v_p,\sigma_p$$ and implements the above dynamics to find the value of $$\phi$$ that maximises the posterior using a manual implementation of the dynamics and iterating using Eulers method.

```python
def simple_dyn():

    # variabels
    v = 2 # real size of item
    sigma_u = 1 # standard deviation of noisy input
    v_p = 3 # mean of prior
    sigma_p = 1 # variance of prior / sensory noise
    s_range = np.arange(0.01,5,0.01) # range of sensory input
    s_step = 0.01 # step size

    # assume that phi maximises the posterior
    phi = np.zeros(np.size(s_range))

    # use Eulers method to find the most likely value of phi
    for i in range(1,len(s_range)):

        phi[0] = v_p
        phi[i] = phi[i - 1] + s_step * ( ( (v_p - phi[i - 1]) / sigma_u ) +
        ( ( v - sensory_transform(phi[i - 1]) ) / sigma_u ) * (2 * phi[i - 1]) ) # equation 12

    # plot convergence
    plt.figure(figsize=(5,2.5))
    plt.plot(s_range,phi)
    plt.xlabel('Time')
    plt.ylabel(r' $\phi$')
    sns.despine()

```

```python
simple_dyn()
```

![png]({{ site.url }}{{ site.baseurl }}/assets/images/Bogacz_8_0.png)

It is clear that the output converges rapidly to $$\phi=1.6$$, the value that maximises the posterior.

So we ask the question: What does a minimal and _biologically plausible_ network model that can do such calculations look like?

---

### Part III - Biological plausibility

Firstly, we must specify what exactly biologically plausible means.

* _A neuron only performs computations on the input it is given, weighted by its synaptic weights._

* _Synaptic plasticity of one neuron, is only based on the activity of pre-synaptic and post-synaptic activity connecting to that neuron._

Consider the dynamics of a simple network that relies on just two neurons and is coherent with the above requirements of local computation

$$ \dot{\epsilon_{p}} = \phi-v_{p}-\Sigma_{p}\epsilon_{p} $$

$$ \dot{\epsilon_{u}} = u-h(\phi)-\Sigma_{s}\epsilon_{s} $$

where $$\epsilon_{p}$$ and $$\epsilon_{s}$$ are the _prediction errors_

$$ \epsilon_{p} = \frac{v_{p}-\phi}{\Sigma_{p}} $$

$$ \epsilon_{s} = \frac{s-g(\phi)}{\Sigma_{s}} $$

that arise from the assumption that the input is normally distributed (again, see Bogaez for derivations).

Below the network dynamics are sketched. Arrows denote excitatory input, circles inhibitory input,   and unless specified ($$\theta,v_p,\Sigma_u,\Sigma_p$$), weights of connections are assumed to be one.

![png]({{ site.url }}{{ site.baseurl }}/assets/images/Bogacz_graph_1.png)

The next snippit of code implements those dynamics and thus, the network "learns" what value of $$\phi$$ that maximises the posterior.

```python
def learn_phi():

    # variabels
    v = 2 # real size of item
    sigma_u = 1 # standard deviation of noisy input
    v_p = 3 # mean of prior
    sigma_p = 1 # variance of prior / sensory noise
    s_range = np.arange(0.01,5,0.01) # range of sensory input
    s_step = 0.01 # step size

    # preallocate
    phi = np.zeros(np.size(s_range))
    epsilon_e = np.zeros(np.size(s_range))
    epsilon_s = np.zeros(np.size(s_range))

    # dynamics of prediction errors for size (epsilon_v) and sensory input (epsilon_u)
    for i in range(1,len(s_range)):

        phi[0] = v_p # initialise best guess (prior) of size
        epsilon_e[0] = 0 # initialise prediction error for size
        epsilon_s[0] = 0 # initialise prediction error for sensory input

        phi[i] = phi[i-1] + s_step*( -epsilon_e[i-1] + epsilon_s[i-1] * ( 2*(phi[i-1]) ) ) # equation 12
        epsilon_e[i] = epsilon_e[i-1] + s_step*( phi[i-1] - v_p - sigma_u * epsilon_e[i-1] ) # equation 13
        epsilon_s[i] = epsilon_s[i-1] + s_step*( v - sensory_transform(phi[i-1]) - sigma_p * epsilon_s[i-1] ) # equation 14

    # plot network dynamics
    plt.figure(figsize=(5,2.5))
    plt.plot(s_range,phi)
    plt.plot(s_range,epsilon_e)
    plt.plot(s_range,epsilon_s)
    plt.ylabel('Activity')
    sns.despine()
```

```python
learn_phi()
```

![png]({{ site.url }}{{ site.baseurl }}/assets/images/Bogacz_11_0.png)

As the figure shows, the network learns $$\phi$$ but is slower in converging than when using Eulers method, as the model relies on several other nodes that are inhibits and excites each other, which causes oscillatory behaviour. Both $$\epsilon_p$$ and $$\epsilon_v$$ oscillate and converge to the values where

$$ \epsilon_{p} \approx 0 $$

$$ \epsilon_{s} \approx 0. $$

Which can be understood as the steady-state of the network. This means that minimising prediction errors (by learning the correct parameters) minimises the free energy potential - a tenet in Active Inference.

---

### Part IV - Approximate estimation of $$\Sigma$$

Recall that we assumed that size $$v$$ was communicated via. a noisy signal $$u$$ assumed to be normally distributed. Above, we outlined a simple sample method for finding the mean value $$\phi$$ that maximises the posterior $$p(v\vert s)$$.

By expanding this simple model, we can esimate the variance $$\Sigma$$ of the normal distribution as well. Considering computation in one single node computing prediction error

$$ \epsilon_{i}=\frac{\phi_{i}-g(\phi_{i+1})}{\Sigma_{i}} $$

where $$\Sigma_{i}=\left\langle (\phi_{i}-g_{i}(\phi_{i+1})^{2}\right\rangle$$ is the variance of the best guess of $$v$$, $$\phi_{i}$$. Estimation of $$\Sigma$$ can be achieved by adding a interneuron $$e_{i}$$ which is connected to the prediction error node, and receives input from this via the connection with weight encoding $$\Sigma_{i}$$, such as sketched in the figure below.

![png]({{ site.url }}{{ site.baseurl }}/assets/images/Bogacz_graph_2.png){:width="250px"}

The dynamics are described by

$$ \dot{\epsilon_{i}} = \phi_{i}-g(\phi_{i+1})-e_{i} $$

$$ \dot{e} = \Sigma_{i}\epsilon_{i}-e_{i} $$

which the following snippit of code implements.

```python
def learn_sigma():

    # variabels
    v = 2 # observed homeostatic error
    sigma_u = 1 # standard deviation of the homeostatic error
    v_p = 3 # mean of prior homeostatic error / noisy input / simple prior
    sigma_p = 1 # variance of prior / sensory noise
    s_range = np.arange(0.01,5,0.01) # range of sensory input
    s_step = 0.01 # step size

    # new variabels
    maxt = 20 # maximum number of iterations
    trials = 2000 # of trials
    epi_length = 20 # length of episode
    alpha = 0.01 # learning rate

    mean_phi = 5 # the average value that maximises the posterior
    sigma_phi = 2 # the variance of phi
    last_phi = 5 # the last observed phi

    # preallocate
    sigma = np.zeros(trials)
    error = np.zeros(trials)
    e = np.zeros(trials)

    sigma[0] = 1 # initialise sigma in 1

    for j in range(1,trials):

        error[0] = 0 # initialise error in zero
        e[0] = 0 # initialise interneuron e in zero
        phi = np.random.normal(5, np.sqrt(2), 1) # draw a new phi every round

        for i in range(1,2000):

            error[i] = error[i-1] + s_step*(phi-last_phi-e[i-1]) # equation 59
            e[i] = e[i-1] + s_step*(sigma[j-1]*error[i-1]-e[i-1]) # equation 60

        sigma[j] = sigma[j-1] + alpha*(error[-1]*e[-1]-1) # synaptic weight (Sigma) update

    # plot dynamics of Sigma
    plt.figure(figsize=(5,2.5))
    plt.plot(sigma)
    plt.xlabel('Time')
    plt.ylabel(r' $\Sigma$')
    sns.despine()
```

```python
learn_sigma()
```

![png]({{ site.url }}{{ site.baseurl }}/assets/images/Bogacz_14_0.png)

Because $$\phi$$ is constantly varying phi = np.random.normal(5, np.sqrt(2), 1) $$\Sigma$$ never converge to just one value, but instead to _approximately_ 2, the variance of $$\phi_i$$.

license: MIT

branch_name: refs/heads/master

extension: md

license_type: permissive


text:
---
lab:
    title: 'Lab 3.1: Create and publish a Knowlege Article in Dynamics 365 Customer Service'
    module: 'Module 3: Learn the Fundamentals of Dynamics 365 Customer Service'
---

# Module 3: Learn the Fundamentals of Dynamics 365 Customer Service

## Practice Lab 3.1 - Create and publish a Knowlege Article in Dynamics 365 Customer Service

### Lab Setup

  - **Estimated Time**: 15 minutes

### Instructions

1. If is not open already, open the **Dynamics 365 Customer Service Hub** application.

2. Using the navigation on the left side of the screen, select **Knowledge Articles**.

3. To easily see the which articles are in different stages, select the drop-down arrow next to **My Active Articles**.

4. Select **Draft Articles**. You will likely see two articles in draft mode.

5. Select **Approved Articles**. You should see at least one approved article.

6. Switch back to **My Active Articles**

7. On the **Command Bar**, select the **New** button.

8. Complete the article as follows:

	- **Title:** `Item Broken on Arrival – your initials`

	- **Keywords:** `Broken Item, Damaged, Return`

	- **Description:** `Helps resolve issues when an Item arrives damaged.`

9. Enter the following text into the Content Designer text.

	Item Arrived Damaged

	When an item arrives damaged, do the following:

	1. Open our web portal

	2. Locate your order record

	3. Select return Item

	4. Select damaged for the reason

	5. Click Print

  Once we have received the returned / damaged item, your account will be credited back the amount.

  **NOTE:** You can add formatting to the text if desired.

10. On the **Command Bar**, select the **Save** button to save the Knowledge Article and leave it open.

11. On the **New Process**, select the **Author** stage, set the **Article Subject** field to **Delivery** (Located under Service).

12. Set the **Mark for Review** field to **Completed**.

13. Select **Next Stage** button to advance to **Review** stage.

14. On the **Command Bar**, select the **Save and Close** button to save your changes and close the article.

After the author initially creates the record, it will generally go through an approval process before it is live. Next, we will act as an approver and approve the article.

15. In the Knowledge Articles, switch the view to **Proposed Articles** to see which articles need your approval.

16. Open the **Item Broken on Arrival – your initials** article you just created.

17. On the **New Process**, select the **Review** stage. Set the **Review** field to **Approved**.

18. You will be asked to confirm the article approval, select **OK**.

19. Click the **Next Stage** button to advance to the **Publish** stage.

20. On the **Command Bar** at the top of the article, select the **vertical ellipsis** at the left of the command bar. From the menu that appears, select **Relate Product**.

21. In the **Relate Product** window, select **Office 365 for Enterprise (Sample).**

22. Click the **Associate** button.

23. On the **New Process**, select the **Publish** stage.

24. Mark the **Set Product Associations** as **Complete**.

25. Set the **Expiration Date** to **one year from today at 12:00 AM**.

26. Click the **Finish** button to complete the process.

27. On the **Command Bar** for the article, click the **Publish** button.

28. Confirm that the following is selected:

	- **Publish:** `Now`

	- **Published Status:** `Published`

	- **Expiration Date:** `One year from today at 12:00 AM`

	- **Expiration State:** `Expired`

	- **Expiration Status:** `Expired`

	- **Publish Approved translations:** `No`

gha_license_id: MIT


text:
---
name: UAA Business Enterprise Institute (BEI)
website: https://www.uaa.alaska.edu/academics/business-enterprise-institute
logo: /images/partners/bei-logo-sm.png
teaser: University of Alaska Anchorage’s Business Enterprise Institute
tagline: Supporting business and entrepreneurial capacities across Alaska by linking economic development programs
---

The University of Alaska Anchorage (UAA) Business Enterprise Institute (BEI) links economic development programs across the University of Alaska (UA) system and supports businesses and entrepreneurial capacities across Alaska. BEI provides a platform for high-level consultancy between industries and UAA.

Business Enterprise Institute ARCTIC project efforts:

* **Design Sprints** and Catalyzer events:
  * Early stage entrepreneurial challenge solving.
* **Startup School**
  * Student accelerator to rapidly develop ideas into viable business models.
* **Entrepreneurial support**
  * Coaching and Technical Assistance
* **Market and Sector Research**:
  * Microgrid market analysis, cluster analysis, commercialization advancement.
* Alaska Startups **Internship Program**:
  * Connecting University of Alaska students with startup market research and business development needs.

gha_language: JavaScript


text:
# Quick Start

Make sure you've read [What is Pinax?](what_is_pinax.md) to get a conceptual overview of Pinax.

We strongly recommend running Pinax (or indeed, any Django) projects in a virtual environment:

```shell
pip install virtualenv
virtualenv mysiteenv
source mysiteenv/bin/activate
pip install pinax-cli
pinax start account mysite
```

If you are using `pipenv` try this instead:

```shell
mkdir mysite
cd mysite
pipenv --three
pipenv shell
pip install pinax-cli
pinax start account mysite --location .
```

**NOTE**: _If you are wondering what `pinax start` actually does, it is equivalent to:_

```shell
pip install Django==2.0
django-admin startproject --template=https://github.com/pinax/pinax-starter-projects/zipball/account mysite
```

### Modern Local Development Steps

If you are using pinax-templates, you will use an npm command to run a script in the package.json file. This script will automatically run the local server and prepare the static files. Install the npm dependencies, install the requirements, initialize your database, load the default sites fixtures, and run the dev server:

```shell
cd mysite
npm install
pip install -r requirements.txt
./manage.py migrate
./manage.py loaddata sites
npm run dev
```

Browse to http://localhost:3000/

#### Collect Static Files for Deployment

To collect the static files run:

```shell
./manage.py collectstatic
```

### Old Local Development Steps

If you are using pinax-theme-bootstrap, you will run the local server by using the Django runserver command. Install the requirements, initialize your database, load the default sites fixtures, and run the dev server:

```shell
cd mysite
pip install -r requirements.txt
chmod +x manage.py
./manage.py migrate
./manage.py loaddata sites
./manage.py runserver
```

Browse to http://<IP_ADDRESS>:8000/

You now have a running Django site complete with account management and pinax-templates or pinax-theme-bootstrap.

## Adding Another Pinax App

Add the new app name to `requirements.txt`:

```python
    # other apps
    pinax-amazing==2.0.1,
```

and install requirements once again.

```shell
pip install -r requirements.txt
```

If you are using `pipenv`, you know to use this instead:

```python
pipenv install pinax-amazing==2.0.1
```

Next, modify `settings.py` by adding your app to `INSTALLED_APPS`:

```python
INSTALLED_APPS = [
    # other apps
    "pinax-amazing",
]
```

This is a good time to make any additional changes to `settings.py` if needed for the new app.

Be sure to establish database tables for the new app:

```shell
./manage.py migrate
```

Finally, modify your project `urls.py` with urls for the new app:

```
    urlpatterns = [
        # other urls
        url(r"^amazing/", include("pinax.amazing.urls", namespace="pinax_amazing")),
    ]
```

This is a good time to adjustment templates for the new app, if needed.

repository: Amanjakhetiya/pinax

repo_name: Amanjakhetiya/pinax


text:
[![CurseForge](https://img.shields.io/badge/CurseForge-DMCLoot-orange)](https://www.curseforge.com/minecraft/mc-mods/dmcloot)
[![Discord](https://img.shields.io/discord/866808032699744306?color=5865F2&label=Discord)](https://discord.gg/ccFpzT5HVF)
# DMCLoot
A Minecraft Mod for 1.16.5 that adds various RPG-like affixes to tools, weapons, and armor!


text:
---
layout: post
title: JS - if, else, else if, switch
subtitle:
categories: dev
tags: js
comments: true
---

### if, else if, else

```javascript
if (condition1) {
  //  block of code to be executed if condition1 is true

} else if (condition2) {
  //  block of code to be executed if the condition1 is false and condition2 is true

} else {
  //  block of code to be executed if the condition1 is false and condition2 is false
}
```

### if else shortcut: conditional operator

- if else

```javascript
condition ? expression_1 : expression_2
```

Like the if statement, the condition is an expression that evaluates to true or false.

If the condition evaluates to true, the operator returns the value of the expression_1; otherwise, it returns the value of the expression_2.

```javascript
age > 18 ? (
    alert("OK, you can register."),
    redirectTo("register.html");
) : (
    stop = true,
    alert("Sorry, you are too young!")
);
```

### switch, break
select one of many code blocks to be executed.

If multiple cases matches a case value, the first case is selected.

If no matching cases are found, the program continues to the default label.

If no default label is found, the program continues to the statement(s) after the switch.

```javascript
switch(expression) {
  case x:
    // code block
    break;
  case y:
    // code block
    break;
     // - It is not necessary to 'break' the last case in a switch block. The block breaks (ends) there anyway.

     // - If you omit the 'break' statement, the next case will be executed even if the evaluation does not match the case.
  default:
    // code block

    // - The 'default' keyword specifies the code to run if there is no case match.
}
```
The switch expression is evaluated once.

The value of the expression is compared with the values of each case.

If there is a match, the associated block of code is executed.

If there is no match, the default code block is executed.

- Example
The getDay() method returns the weekday as a number between 0 and 6.

(Sunday=0, Monday=1, Tuesday=2 ..)

```javascript
switch (new Date().getDay()) {
  case 0:
    day = "Sunday";
    break;
  case 1:
    day = "Monday";
    break;
  case 2:
     day = "Tuesday";
    break;
  case 3:
    day = "Wednesday";
    break;
  case 4:
    day = "Thursday";
    break;
  case 5:
    day = "Friday";
    break;
  case 6:
    day = "Saturday";
}
```

```javascript
switch (new Date().getDay()) {
  case 4:
  case 5:
    text = "Soon it is Weekend";
    break;
  case 0:
  case 6:
    text = "It is Weekend";
    break;
  default:
    text = "Looking forward to the Weekend";
}
```

- The 'default' case does not have to be the last case in a switch block:

 - If 'default' is not the last case in the switch block, remember to end the default case with a break.

 ```javascript
 switch (new Date().getDay()) {
  default:
    text = "Looking forward to the Weekend";
    break;
  case 6:
    text = "Today is Saturday";
    break;
  case 0:
    text = "Today is Sunday";
}
```


text:
---
layout: post
date: '2016-02-14'
title: "Bonny Bridal Bonny Classic 927 Simple Chiffon Wedding Dress"
category: Bonny Bridal
tags: [Bonny Bridal]
---
### Bonny Bridal Bonny Classic 927 Simple Chiffon Wedding Dress
Just **$315.99**
###

Beaded straps fall into the shirred V bodice. The shirred empire waist is highlighted by a center cluster of beading. The skirt and extends to the chapel train that is decorated by scattered appliques.

Available in sizes 2-32.

Buy it: [https://www.eudances.com/en/bonny-bridal/290-bonny-classic-927-simple-chiffon-wedding-dress.html](https://www.eudances.com/en/bonny-bridal/290-bonny-classic-927-simple-chiffon-wedding-dress.html)


text:
# scap
A minimal (read "garbage") screen capture script based on scrot and ffmpeg. I made it for my own personal entertainment and it messes up any output format other than gifs if I recall correctly.

## Dependencies
 - scrot
 - ffmpeg
 - bc

## Instal
### linux
```sh
sudo ./install
# or
doas ./install
```

## Usage
```sh
scap [duration in seconds] [output file name] [additional scrot arguments...]
```
Example:
```sh
scap 10 ~/test.gif -p -u
```
Output:
 - a gif
 - 10 seconds long
 - `-p` : enables pointer capture for scrot
 - `-u` : makes scrot track a specific window

## TODO
 - [ ] improve framerate
 - [ ] fix the awful mp4 output

license: Unlicense

repository: LukasDrsman/scap

branch_name: refs/heads/main

repo_name: LukasDrsman/scap


text:
# "Bullet" physics for node.js

## The Basics
* Only works on linux at the moment
* Very limited binding types
* Requires bullet to be built in /libbullet with libbullet_build.sh
* Bullet is statically linked into the module

## Notes to self
* Full reset with git fetch --all; git reset --hard origin/master
* Build with node-gyp configure && node-gyp build -v

repository: deniszatsepin/node-bullet

repo_name: deniszatsepin/node-bullet


text:
---
layout: default
---

# 1993-01-15 - Re: possible solution to the anonymous harrassment problem

## Header Data

From: Derek Atkins<EMAIL_ADDRESS>To<EMAIL_ADDRESS>Message Hash: 07b2fc05cabf10460922e611658d84ee2ceb847a6734c794e7148129fd104293

Message ID<EMAIL_ADDRESS>Reply To<EMAIL_ADDRESS>UTC Datetime: 1993-01-15 21:41:59 UTC

Raw Date: Fri, 15 Jan 93 13:41:59 PST

## Raw message

```
{% raw  %}From: Derek Atkins<EMAIL_ADDRESS>Date: Fri, 15 Jan 93 13:41:59 PST
To<EMAIL_ADDRESS>Subject: Re: possible solution to the anonymous harrassment problem
In-Reply-To<EMAIL_ADDRESS>Message-ID<EMAIL_ADDRESS>MIME-Version: 1.0
Content-Type: text/plain

> I thought their interface was good enough to do all of the obvious
> operations -- RSA block encrypt and decrypt being the most important --
> and that this restriction was just to prevent bizarrelly hacked
> versions of their code from being confused with the original.
>
> >       R_SignPEMBlock     computes a digital signature on a message
> > R_VerifyBlockSignature   verifies a digital signature on a block of
> >                            data such as a certificate
>
> Let me know if I'm wrong, but I don't think I am.

You are wrong.  The interface does *not* give you RSA Block
De/Encrypt.

-derek

{% endraw %}
```

## Thread

+ Return to [January 1993](/archive/1993/01)

+ Return to "[Derek Atkins <warlord@MIT.EDU>](/authors/derek_atkins_warlord_at_mit_edu_)"
+ Return to "[Marc.Ringuette@GS80.SP.CS.CMU.EDU](/authors/marc_ringuette_at_gs80_sp_cs_cmu_edu)"

+ 1993-01-15 (Fri, 15 Jan 93 12:30:20 PST) - [Re: possible solution to the anonymous harrassment problem](/archive/1993/01/7a45912047ad1efa18aeae3dd95af18c5f1a2c56b5ff8582c11a291c99551e27) -<EMAIL_ADDRESS>  + 1993-01-15 (Fri, 15 Jan 93 13:41:59 PST) - Re: possible solution to the anonymous harrassment problem - _Derek Atkins<EMAIL_ADDRESS>


text:
---
title: R Basics
description_seo: description for seo and card use
duration: "17:36"
keywords:
programming_lang: R
venue:
location:
author: Chris Bail
author_title: Professor
is_bootcamp: true
date_published:
has_order: 03
preview: https://i.ytimg.com/vi/vVcH_OvrLEM/hqdefault.jpg
video_url: https://www.youtube.com/watch?v=vVcH_OvrLEM
embed_url: https://www.youtube.com/embed/vVcH_OvrLEM
materials:
  - title: Coronavirus Tweets Dataset
    url: https://compsocialscience.github.io/summer-institute/assets/datasets/Coronavirus_Tweets.Rdata
  - title: Bootcamp Solutions
    url: https://compsocialscience.github.io/summer-institute/boot_camp/bootcamp_answers.pdf
resources:
  - title: R for Data Science (Chapter 4)
    url: https://r4ds.had.co.nz/workflow-basics.html
exercises:
  - title: R Basics Quiz
    url: /boot_camp/r_basics
code:
---

Create and name different types of objects (e.g. vectors and dataframes) and learn about different classes of objects (e.g. numeric vs. string) as well as special features that make RStudio easier to use.

repository: compsocialscience/summer-institute

gha_language: HTML

repo_name: compsocialscience/summer-institute


text:
---
title: "Links for 2018-11-20"
layout: post
date: 2018-11-20
---

* [Exploring Plug: The Body Reader](https://words.saulecabrera.com/posts/exploring-plug-the-body-reader/)
* [htop: Here’s how to customize it](https://haydenjames.io/htop-heres-how-to-customize-it/)
* [Get stuff done with Kubernetes](https://argoproj.github.io/)
* [Why Great Managers Matter](https://open.buffer.com/why-great-managers-matter/)
* [Kubernetes Port Forwarding for Local Development](https://imti.co/kubernetes-port-forwarding/)

gha_language: CSS


text:
# ShelfAwareness

## Project Description:

A 'personal catalog' of books. Users will be able to do the following:

    1. Check off books they own
    2. Check off books they have read already
       - Rate the books they've read
       - Record favorite quotes
       - Write notes about those books
       - Write reviews of those books
       - Write analyses of those books
       - Start discussions about those books
    3. Mark books that they are in the proccess of reading
    4. Mark books they want to/intend to read
    5. Find other books they may be interested in
       - Popular books in the same genre
       - Books by authors of works they've already read
       - Further reading of books suitable for age group
           - Lexile (service for teachers)
    6. Create customized lists/collections of books, based on genre, themes, etc.
    7. Create a favorites list
    8. View the profiles of everything above from other users
       - View the most popular books and authors on the site
    9. Add books to a wishlist if they cannot afford books
       - Wishes are moved to a queue and other users will have the option to donate or sell at a discounted price
    10. Invite others to use the service
       - Some form of compensation
       - Top contributors to wishlists are also recognized on site

## Intent
To encourage literacy in children (or adults), and allow those without access to books to possibly get them


text:
# Installing Distgen

##  Using conda

```bash
conda install -c conda-forge pytao
```

## Using setuptools

```bash
python setup.py install
```

## Developers

Clone this repository:
```shell
git clone https://github.com/ColwynGulliford/distgen.git
```

Create an environment `distgen-dev` with all the dependencies:
```shell
conda env create -f environment-dev.yml
```

Install as editable:
```shell
conda activate distgen-dev
pip install --no-dependencies -e .
```

Create documentation:
```shell
mkdocs serve
```

repository: ColwynGulliford/distgen

gha_language: Python

repo_name: ColwynGulliford/distgen


text:
+++
title = "February 2023"
date = "2023-02-01"

[featured-1]
title = "Realm"
description = "Realm is a desktop Urbit interface from that offers a variety of integrated features."
image="https://storage.googleapis.com/media.urbit.org/site/ecosystem/applications/realm-hero.png"
content = """

Realm proposes an Urbit experience that is outside the browser, running as a full-screen cross-platform native application. It offers features like shared application suites, built-in audio chatrooms, an integrated crypto wallet, as well as its own web browser.

![](https://media.urbit.org/site/featured/realm-screenshot.jpg)

Realm is the flagship product of Holium, who are also building out several collaboration tools akin to a cloud productivity suite for Urbit and Realm.  These applications can be bundled together into unique spaces – desktop environments that have been configured for communities and teams.

![](https:///media.urbit.org/site/ecosystem/applications/app-suite.png)

Realm is currently in private alpha.  Visit [holium.com](https://holium.com) to sign up for the invitation waitlist.  In the meantime, you can also enjoy an [entertaining podcast](/podcasts/2023-01-24_reject-triviality) in which Holium founder `~lomder-librun` talks about his vision for Realm, amongst many other interesting topics.

"""

[featured-2]
title = "Native Planet"
description = "Native Planet is building Urbit-native hardware as well software which enables standalone Urbit home servers."
image="https://storage.googleapis.com/media.urbit.org/site/ecosystem/spotlight/native-planet-thumb.jpg"
content = """

Native Planet is Urbit's first dedicated hardware company.  Their first product, the [Tellurian](https://www.nativeplanet.io/hardware), is a turnkey Urbit computer that you can run at home and access anywhere thanks to Native Planet's open-source [software](https://www.nativeplanet.io/software).

![Screenshot](https://storage.googleapis.com/media.urbit.org/site/getting-started/native-planet.jpg)

What's the point of having a physical Urbit computer, besides the fact that they look very cool?

You get the best of both worlds: the accessibility of cloud hosting, with the ownership of running Urbit locally.  Groundseg and Startram make your Urbit accessible to any networked device without the need to trust any cloud service provider.

"""

[featured-3]
title = "Urbit for Idiots | Galen Wolfe-Pauly, Tlon Corporation"
description = "Tlon CEO Galen Wolfe-Pauly talks to the Boys Club ladies and expounds on the fundamentals of Urbit."
image=""
content = """

Is Urbit a computer? Is owning 'space' on the internet valuable? What is Urbit? How is it different from the the existing internet?  Galen and Boys Club get to the bottom of these evergreen topics.
"""
+++


text:
# Gittr

A command line utility to track time using Toggl and Gitlab issues
based on the current checked out branch of a repository.

## Installation

    npm install -g gittr

## Usage

### Configuration

First you must indicate your Gitlab API token, Toggl API token
and repository path.

In order to do that you can run `gittr` with no arguments,
and it will prompt for each of these settings.

    gittr

There is no need to specify Gitlab's server url, it is
automatically retrieved from the repository's `origin` remote.

To reset the configuration:

    gittr reset-config

To reconfigure the repository path:

    gittr set-repository [repository-path]

### Toggl project

You need to create a Toggl project manually.
The project name must match the format: `namespace/project` from
your Gitlab repository.

### Timing

To start a new timer:

    gittr start

This will start a timer with a description set to the current branch name
of the configured repository.

To stop the timer:

    gittr stop

This will stop the toggl timer. If the current branch name matches a Gitlab issue
branch format (`id-issuename`), it will also inform gitlab on the time spent
working on the issue.

To print the current timer:

    gittr current

Here, `repository-path` is an absolute or relative path to the repository.
The argument defaults to the current working directory when not specified.

repository: albertsgrc/gittr

repo_name: albertsgrc/gittr


text:
# Todo List
The goal of this repository is to create a todo list app where a user can authenticate and get their to do list

# Requirements
- User is required to authenticate
- After logging in, user can create multiple todo lists
- Each list should be able to add items and mark things as completed
- Each list item should be able to be re-organized

repository: FunWithPythonProgramming/todo-list

repo_name: FunWithPythonProgramming/todo-list


text:
---
title: Impact Analysis
description: Using the Nexosis API to determine the Impact of an event on your data
category: Forecasting
tags: [impact analysis]
use_codestyles: true
order: 4
---

Impact analysis is when we analyze your historical time series data and determine the impact of internal and external factors. You can use the predictive power of impact analysis to evaluate the impact of an event, promotion, limited time offer, etc. on your bottom line, determine impact of weather or illness on productivity, or understand how holidays will impact sales.

-----

### Creating an Impact Session

#### Impact sessions determine the impact of a particular event on a dataset. To create an impact session, specify the dataset for which to determine impact, as well as the start and end dates of the impactful event. The Nexosis API will execute a series of machine learning algorithms to determine the impact of the event on the dataset.

> Both the start and end dates for the impact session must always be on or before the specified timestamp of the last record in your dataset.

_To understand how to submit data, you can read more in the [Sending Data](/guides/sending-data) article._

**Here are the parameters you can include in either the query string or the body of a POST request to create an Impact Analysis Session:**
* `dataSourceName` - Name of the data source (dataset or view) for which to determine impact
* `targetColumn`- Column in the specified dataset for which to determine impact
* `eventName` - Name of the event for which to determine impact
* `resultInterval` - The interval at which predictions should be generated. Possible values are `Hour`, `Day`, `Week`, `Month`, and `Year`. Defaults to `Day`
* `startDate` - Format date-time (as date-time in ISO8601). First date of the event
* `endDate` - Format date-time (as date-time in ISO8601). Last date of the event
* `callbackUrl` - The Webhook URL that will receive updates when the Session status changes

### Starting an Impact Session

#### Impact sessions are essentially identical to forecast sessions, so make sure to read and understand how to [create predictions](forecasting-walkthrough). All of that information will apply with a couple of additional points that will be outlined in the rest of this section.

**Here are the differences:**

1. Parameters include an additional value called `eventName` so you can create a friendly name for the intervention period.
2. Impact session results also include metrics that describe the overall impact of the event on the dataset. These metrics are:
    * `pValue` - Statistical value used to determine the significance of the impact. A small p-value indicates strong evidence of impact, whereas a p-value approaching 0.5 indicates weak evidence of impact.
    * `absoluteEffect` - Total absolute effect of the event on the dataset. Answers the question, "How much did this event affect my dataset?"
    * `relativeEffect` - Percentage effect of the event on the dataset. Answers the question, "By what percentage did this event affect my dataset?"

>IMPORTANT: If you want to find the impact a particular feature had on the target value, you must set that feature's value off during the dates of the intervention period otherwise it will not measure the impact correctly. Impact session results consist of the predictions of what would have happened over the specified date range, had the impactful event not occurred, which is why that feature should be removed from the intervention period.


text:
<!-- Do not edit this file. It is automatically generated by API Documenter. -->

[Home](./index.md) > [gatsby-plugin-next-seo](./gatsby-plugin-next-seo.md) > [LocalBusinessJsonLdProps](./gatsby-plugin-next-seo.localbusinessjsonldprops.md) > [openingHours](./gatsby-plugin-next-seo.localbusinessjsonldprops.openinghours.md)

## LocalBusinessJsonLdProps.openingHours property

The opening hours of a certain place.

<b>Signature:</b>

```typescript
openingHours?: OpeningHoursSpecification | OpeningHoursSpecification[];
```

## Remarks

Use both the validFrom and validThrough properties to define seasonal hours. This example shows a business closed for winter holidays.

\#\#\#\# Standard hours

Excluding the validFrom and validThrough properties signify that the hours are valid year-round.This example defines a business that is open weekdays from 9am to 9pm, with weekend hours from 10am until 11pm.

```js
const props = {
  ...other,
  openingHoursSpecification: [
    {
      dayOfWeek: [
       "Monday",
       "Tuesday",
       "Wednesday",
       "Thursday",
       "Friday"
      ],
      opens: "09:00",
      closes: "21:00"
    },
    {
      dayOfWeek: ["Saturday", "Sunday"],
      opens: "10:00",
      closes: "23:00"
    }
  ]
}

```
\#\#\#\# Late night hours

For hours past midnight, define opening and closing hours using a single OpeningHoursSpecification property. This example defines hours from Saturday at 6pm until Sunday at 3am.

```js
const props = {
  ...other,
  openingHoursSpecification: {
    opens: "18:00",
    closes: "03:00",
    dayOfWeek: "Saturday",
  }
}

```
\#\#\#\# All-day hours

To show a business as open 24 hours a day, set the open property to "00:00" and the closes property to "23:59".To show a business is closed all day, set both opens and closes properties to "00:00". This example shows a business open all day Saturday and closed all day Sunday.

```js
const props = {
  ...other,
  openingHoursSpecification: [
    {
      dayOfWeek: "Saturday",
      opens: "00:00",
      closes: "23:59"
    },
    {
      dayOfWeek: "Sunday",
      opens: "00:00",
      closes: "00:00"
    }
  ]
}

```
\#\#\#\# Seasonal hours

```js
const props = {
  ...other,
  openingHoursSpecification: {
    opens: "00:00",
    closes: "00:00",
    validFrom: "2015-12-23",
    validThrough: "2016-01-05"
  }
}

```

repository: ifiokjr/gatsby-plugin-next-seo

gha_language: TypeScript

repo_name: ifiokjr/gatsby-plugin-next-seo


text:
# Pantilt unit

## Run
Run the pantilt with:
```bash
cd ~/catkin_ws/src/vision/src/flir_pantilt_d46
roslaunch launch/diana.launch
```

Move the pantilt using the bash script:
```bash
cd /home/diana/Scripts
```
This will set the pantilt to 0.4 pan and 0 tilt:
```bash
./movePantilt.sh 0.4 0
```

Move the pantilt manually:

```bash
rostopic pub /ptu/cmd sensor_msgs/JointState "header:
  seq: 0
  stamp: {secs: 0, nsecs: 0}
  frame_id:
name: ['pan', 'tilt']
position: [$pan_target, $tilt_target]
velocity: [0.1, 0.1]
effort: [0]"
```

## Troubleshooting

Sometime the connection computer-pantilt controller does not work. You can attempt this command in order to enstablish a connection:

```bash
for a in $(seq 0 1000); do
  echo 'a' > /dev/ttyUSB0
done
```

Then try to restart the connection.


text:
Sea turtles are miraculous.
First, they've been around
since the late Jurassic,
roughly 150 million years ago.
Cohorts of the dinosaurs,
sea turtles have survived
through the challenges of eons,
existing still today,
where many others
have ended their evolutionary run.
Second, throughout the centuries
and up till today,
every living adult sea turtle
has overcome the odds,
existing as a consequence of chance,
skill, and capability.
The gauntlet each sea turtle faces

in the course of its lifetime goes thus:
First, deposited as a clutch of leathery,
ping-pong ball-sized eggs
into a nesting pit dug by its mother
high on the beach,
of the 50 to 200 eggs laid,
roughly 20 percent will never hatch.
Roughly a month and a half
after having been laid,
the surviving eggs hatch,
and the young turtles, each small enough
to fit in the palm of your hand,
squirm to the surface,
emerging from the sand en masse,
and making their desperate
dash for the sea.
Along the way, debris, pitfalls, crabs,
gulls, raccoons, and other threats
will claim roughly 50 percent of those
who rose from the sand.
For those that actually reach the surf,
they trade one set of threats for another,
as they first face
the repelling force of the waves,
and then find a whole new

host of predators awaiting them:
Various fish, dolphins,
sharks, and sea birds,
as the young turtles
come to the surface for air.
For their first few days of life,
should they count themselves
amongst the living,
the vulnerable turtles
swim frantically forward.
Ultimately, they will often
look to settle in a patch of flotsam,
preferably a patch of floating seaweed.
Now for the next several months,
they will seek to avoid
those that would eat them,
find that which they might eat themselves,
and not fall to the pressures
of challenging weather
or unfortunate currents.
In this phase, roughly 50 percent
of those who reach the surf
will perish.
Ultimately, with the passage of years,
the survivors will increase in size,
from that of a dinner plate at year one
to that of a dinner table,
in the case of one species
at least, the leatherback,
a decade or so later.
With size comes
some measure of protection.
The only truly worrisome predators
now are some of the larger shark species--
bulls, tigers, and whites --
and the occasional killer whale.
At approximately two decades of age,
the survivors will be old enough
themselves to breed,
and continue the cycle
which their very existence heralds.
Of those that began
as eggs on a distant beach,
now less than 10 percent remain,
at least, those were the odds
prior to significant human interference.
Over the past century, and in particular
in the last several decades,
human endeavors, from beach development
to plastic refuse to poaching,
long lines, nets,
and even noxious chemicals, including oil,
have upped the ante for sea turtles,
causing their survival rate to drop
to around one percent or less,
from each nesting cycle.
It is this added human pressure
which has pushed
each of the eight sea turtle species
into either a threatened
or endangered state.
For while they have evolved
to overcome a host of obstacles,
the most recent has arisen so quickly
and at such scale that the species
find themselves overwhelmed.
So let's quickly recap this cycle of odds.
Using a hypothetical nesting season,
for females may nest
multiple times in a single year,
of 1,000 eggs, for sake of ease.
1000 eggs laid.
800 hatch.
400 make it to the water.
200 progress toward adulthood.
20 survive to breeding age --
that is, without human interference.
Two survive to breeding age
with human interference.
So a breeding adult sea turtle
is the very embodiment of a long shot.
It is the exception, not the rule.
A jackpot.
It is, in a very real sense,
a miracle.

repository: prewittdavon/TEDVis

repo_name: prewittdavon/TEDVis


text:
# domeneshop-dns-updater

As domeneshop is missing an API, this small util provides an automated way to update the _acme-challenge TXT record needed for certbot automatic renewals

# 1. Run from host

## Install
```sh
pip install -r requirements.txt
```

## Configure
```sh
cp config.yml-default config.yml
```

Add username and password, id for domain (7 digits) and the domains to update.

## Run

```sh
certbot certonly --manual --manual-auth-hook domeneshop.py --agree-tos --manual-public-ip-logging-ok -d <domain.name>

```

## Certbot-config
Make sure your renewal-config contains the following:
### /etc/letsencrypt/renewal/domain.name.conf
```
pref_challs = dns-01,
server = https://acme-v02.api.letsencrypt.org/directory
authenticator = manual
installer = None
manual_public_ip_logging_ok = True
manual_auth_hook = /path/to/domeneshop-dns-updater/domeneshop.py

```

# Credit

Forked from https://github.com/runelangseid/domeneshop-dns-updater

repository: Olen/domeneshop-dns-updater

repo_name: Olen/domeneshop-dns-updater


text:
Hapi.js
=====================

## Description

Learn how to take your application to the next level.  With hapi.js training you will learn about the internals of hapi.js as well as how to use it to enable teams to build web applications and services.

## With this training, you will learn

How to create a micro-services tier using [Hapi.js](http://hapijs.com/) including distributed plugin development, testing hapi servers, builds, and deployment. Included will be the resources and knowledge to be able to help other groups do the same thing.

## Trainers

* [Ben Acker]()
* [Wyatt Preul](http://jsgeek.com)
* [Van Nguyen]()

## Preparations for this training

In order to prepare to this training you should/must do the following List of readings and exercises. If you have questions, please open an issue and we will be glad to answer, you might be helping other participants too.

### TODO List

* Complete some of the [makemehapi](https://github.com/spumko/makemehapi) workshopper.
* Come up with an API that you would like to build, nothing too fancy, just a few endpoints that you would like to expose. It could be anything you like, here are some data source ideas:
    * An API that exists but you'd like to make it better
    * A combination of a few different publicly accessible APIs
    * A site that has data in HTML but not no data API to serve the data

Some places to find inspiration for data and APIs:
* [Portugal's Open Data](http://www.dados.gov.pt/pt/inicio/inicio.aspx)
* [EU Open Data](https://open-data.europa.eu/en/data/)
* [Fire data from Portugal](http://www.incendios.pt/pt)
* [Programmable Web](http://www.programmableweb.com/)

### Materials

* Laptop
* hapi.js installed

## 28 jun - 17:30h Participants

- André Cruz - [satazor](https://github.com/satazor)
- André Santos - [andrefs](https://github.com/andrefs)
- David McMullin - [davecocoa](https://github.com/davecocoa)
- Dominykas Blyžė - [dymonaz](https://github.com/dymonaz)
- Filipe Dias - [filipediasferreira](https://github.com/filipediasferreira)
- George Shank - [taterbase](https://github.com/taterbase)
- Joaquim Serafim - [joaquimserafim](https://github.com/joaquimserafim)
- John Brett - [johnbrett](https://github.com/johnbrett)
- Marcelo Conceição - [marcelombc](https://github.com/marcelombc)
- Marco Oliveira - [marcooliveira](https://github.com/marcooliveira)
- Miguel Pereira - [miguelampereira](https://github.com/miguelampereira)
- Paulo Vieira - [paulovieira](https://github.com/paulovieira)
- Ricardo Melo - [rjsmelo](https://github.com/rjsmelo)
- Zoltan Feher - [zkiiito](https://github.com/zkiiito)

## 27 jun - 14:30h Participants

- Daniel da Silva - [danielfdsilva](https://github.com/danielfdsilva)
- James Nocentini - [jamiltz](https://github.com/jamiltz)
- João Jerónimo - [joaojeronimo](https://github.com/joaojeronimo)
- Luke Bond - [lukebond](https://github.com/lukebond)
- Marco Pantaleo - [peeofive](https://github.com/peeofive)
- Ricardo Quintas - [rdquintas](https://github.com/rdquintas)
- Robert Kowalski - [robertkowalski](https://github.com/robertkowalski)
- Sandro Maio - [sandromaio](https://github.com/sandromaio)
- Stefan Jansen - [xtravanta](https://github.com/xtravanta)
- Tiago Rodrigues - [trodrigues](https://github.com/trodrigues)
- Tom Cartwright - [tomcartwrightuk](https://github.com/tomcartwrightuk)

repository: nvcexploder/training-hapijs

repo_name: nvcexploder/training-hapijs


text:
# Konva Website

The website for Konva. Created with Hexo framework.
You can see the generated files at [konvajs/konvajs.github.io](https://github.com/konvajs/konvajs.github.io) repository.

## How to help?

We need to replace jsbin code examples with iframe example and code snippet.
All demos will be stored in this repo. It will much ease to maintain them.

You can see `source/docs/shapes/Rect.md` (docs) and `source/downloads/code/shapes/rect.html` (working code snippet).
All demos should be stored under `source/downloads/code`.

## Getting started

Install dependencies:

``` bash
$ git clone https://github.com/konvajs/site.git
$ cd site
$ npm install
```

Generate:

``` bash
$ gulp generate
```

Run server:

``` bash
$ gulp server
```

## Requirements

- [Hexo](http://hexo.io/)

	``` bash
  $ npm install hexo -g
  ```

- [Gulp](http://gulpjs.com/)

	``` bash
	$ npm install gulp -g
	```

repository: johnhomes/site

repo_name: johnhomes/site


text:
# Product marketing hierarchy

A product hierarchy is a way of organizing our products and features. As we evolve from offering a single product to multiple products and features, having a clear product hierarchy helps marketing prioritize our efforts, make naming decisions, ensure consistent style guidelines, etc.

Only L1 products that are Generally Available (GA) will have dedicated product landing pages and inclusion on the about site homepage.

Our product hierarchy will be updated as we launch new products and features. Here is the current hierarchy as of 2021-04-08:

![Product Hierarchy](https://user-images.githubusercontent.com/20098595/114071417-b2df5900-9866-11eb-897c-7b0438e62c46.jpg)

repository: zag/about

repo_name: zag/about