robstewart57

-- | Compares the structure of two graphs and returns 'True' if their
--   graph structures are identical. This does not consider the nature
--   of each node in the graph, i.e. the URI text of 'UNode' nodes,
--   the generated index of a blank node, or the values in literal
--   nodes. Unsafe because it assumes IRI resolution will succeed, may
--   throw an 'IRIResolutionException` exception.
isGraphIsomorphic :: (Rdf a, Rdf b) => RDF a -> RDF b -> Bool
isGraphIsomorphic g1 g2 = Automorphism.isIsomorphic g1' g2'
  where
    g1' = rdfGraphToDataGraph g1

robstewart57

Using Theano backend.
('X_train shape:', (60000, 1, 28, 28))
(60000, 'train samples')
(10000, 'test samples')
____________________________________________________________________________________________________
Layer (type)                     Output Shape          Param #     Connected to                     
====================================================================================================
convolution2d_1 (Convolution2D)  (None, 32, 26, 26)    320         convolution2d_input_1[0][0]      
____________________________________________________________________________________________________
activation_1 (Activation)        (None, 32, 26, 26)    0           convolution2d_1[0][0]            

robstewart57

ones : List Nat -> List Nat
ones = map (const 1)

f : (input:List Nat) -> (sum (ones input) = length input)
f input = case input of
               [] => Refl
               (x::xs) => ?hole

robstewart57

ffBench.hs:34:25:
    Could not deduce (Applicative m) arising from a use of ‘pure’
    from the context (Monad m)
      bound by a type expected by the context:
                 Monad m => m s -> (s -> m ()) -> m b
      at EffBench.hs:(33,20)-(34,34)
    Possible fix:
      add (Applicative m) to the context of
        a type expected by the context:
          Monad m => m s -> (s -> m ()) -> m b

robstewart57

data Foo : Vect m (Nat,Type) -> Vect n (Nat,Type) -> Type where
  Bar : {x:List Nat}
     -> {y:List Nat}
     -> (Vect m x -> Vect n y)
     -> Foo ?rhs1 ?rhs2

-- examples:
f : Foo [(2,Nat),(1,Nat)] [(1,Nat)]
f = Bar (\[ [x,y] , [z] ] => [ [x+y+z] ])

robstewart57

-- works nicely.
headEq'' : DecEq a => (x : a) -> (ys : List a) -> NonEmpty ys -> Dec (x = head ys)
headEq'' x (y :: ys) IsNonEmpty =
   -- just return the result of `decEq`
   decEq x y

-- see:
headEq'' 1 [1, 2] : NonEmpty [1, 2] -> Dec (1 = 1)

-- what about just pattern matching on the result

robstewart57

import Data.Vect

-- earlier in the docs:

-- http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#case-expressions
--
-- Another way of inspecting intermediate values of simple types is to
-- use a case expression.
my_filter_case : (a -> Bool) -> Vect n a -> (p ** Vect p a)
my_filter_case p [] = ( _ ** [] )

robstewart57

consider this Haskell:

import Prelude hiding (sum,length)

mean_good :: [Int] -> Double
mean_good xs = go 0 0 xs
  where
    go !accum !denom [] =
      fromIntegral accum / fromIntegral denom
    go !accum !denom (!x:xs) =

robstewart57

stack -v install criterion
Version 1.1.0, Git revision 0e9430aad55841b5ff2c6c2851f0548c16bce7cf (3540 commits) x86_64 hpack-0.13.0
2016-05-14 11:43:24.717228: [debug] Checking for project config at: /home/rob/code/haskell/bones-knapsack/stack.yaml @(stack_4KUX0HKhK5M2TdLcUMZ5Rt:Stack.Config src/Stack/Config.hs:792:9)
2016-05-14 11:43:24.717568: [debug] Loading project config file stack.yaml @(stack_4KUX0HKhK5M2TdLcUMZ5Rt:Stack.Config src/Stack/Config.hs:810:13)
2016-05-14 11:43:24.719575: [debug] Checking whether stack was built with libgmp4 @(stack_4KUX0HKhK5M2TdLcUMZ5Rt:Stack.Config src/Stack/Config.hs:327:5)
2016-05-14 11:43:24.719792: [debug] Run process: ldd /usr/bin/stack @(stack_4KUX0HKhK5M2TdLcUMZ5Rt:System.Process.Read src/System/Process/Read.hs:283:3)
2016-05-14 11:43:24.729313: [debug] Stack was not built with libgmp4 @(stack_4KUX0HKhK5M2TdLcUMZ5Rt:Stack.Config src/Stack/Config.hs:331:14)
2016-05-14 11:43:24.729605: [debug] Trying to decode /home/rob/.stack/build-plan-cache/x86_64-linux/lts-5.12.ca

robstewart57

main = do
  let a = enumFromN (index2 2 3) 1          :: Acc (Array DIM2 Int)
  let b = enumFromStepN (index2 2 3) 6 (-1) :: Acc (Array DIM2 Int)
  run $ A.zipWith (+) a b