turion

Verifying that +turion is my Bitcoin username. You can send me #bitcoin here: https://onename.io/turion

turion

 * Package:    sci-mathematics/agda-2.4.2.5
 * Repository: haskell
 * Maintainer: sci-mathematics@gentoo.org haskell@gentoo.org
 * USE:        abi_x86_64 amd64 cpphs doc elibc_glibc hoogle kernel_linux stdlib userland_GNU
 * FEATURES:   preserve-libs sandbox userpriv usersandbox
>>> Unpacking source...
>>> Unpacking Agda-2.4.2.5.tar.gz to /var/tmp/portage/sci-mathematics/agda-2.4.2.5/work
>>> Source unpacked in /var/tmp/portage/sci-mathematics/agda-2.4.2.5/work
>>> Preparing source in /var/tmp/portage/sci-mathematics/agda-2.4.2.5/work/Agda-2.4.2.5 ...
 * CHDEP: 'zlib >= 0.4.0.1 && < 0.6.1' -> 'zlib >= 0.4.0.1'

turion

record Live a where
  constructor LiveC
  state : Type
  step : state -> (a, state)

bind : Live (Live a) -> Live a
bind {a} (LiveC state1 step1) = LiveC newstate f where
  f (sta1 ** st2) = (?aVal, (?st1' ** ?st2'))
  newstate : Type
  newstate = (st1 : state1 ** state (fst (step1 st1)))

turion

import Prelude hiding ((.), id)
import Control.Category
import Control.Arrow

data Stream a = Stream
  { headS :: a
  , tailS :: Stream a
  }
  deriving Show

turion

{-# LANGUAGE DataKinds #-}
data Cell m a b = ...

instance Monad m => Arrow (Cell m) where
  arr :: (a -> b) -> Cell m a b
  (***) :: Cell m  a1       b1
        -> Cell m      a2       b2
        -> Cell m (a1, a2) (b1, b2)

instance Monad m => Functor (Cell m a) where

turion

{-# LANGUAGE ApplicativeDo #-}
module StreamT where

-- base
import Control.Arrow

data StreamT m a = StreamT { unStreamT :: m (a, StreamT m a) }

instance Functor m => Functor (StreamT m) where
  fmap f = StreamT . fmap (f *** fmap f) . unStreamT

turion

data ProbT m a where
  ProbT :: m [(Double, a)] -> ProbT m a -- sum double = 1
  | GaussianDist
      :: Double -- | Mean
      -> Double -- | Width
      -> ProbT m Double
  | ...
return a = [(1, a)]

-- Real system

turion

{-# LANGUAGE Arrows #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TupleSections #-}

-- base
import Control.Arrow
import Control.Category
import Control.Concurrent
import Control.Monad (guard, (>=>), void)