bigs

const CHUNK_SIZE = 50;

class FetchUsers implements AsyncIterable<string> {
  #users: string[]; 
  #chunk: number;

  constructor() {
    this.#chunk = 0;
    this.#users = [];
  }

bigs

diff --git a/x/wasm/alias.go b/x/wasm/alias.go
index 610ce97..3e32935 100644
--- a/x/wasm/alias.go
+++ b/x/wasm/alias.go
@@ -17,7 +17,6 @@ const (
 	TStoreKey                       = types.TStoreKey
 	QuerierRoute                    = types.QuerierRoute
 	RouterKey                       = types.RouterKey
-	MaxWasmSize                     = types.MaxWasmSize
 	MaxLabelSize                    = types.MaxLabelSize

bigs

module Arity

import Data.Vect

export
repeat : {n : Nat} -> a -> Vect n a
repeat {n = 0} _ = []
repeat {n = S n} x = x :: repeat {n} x

export

bigs

module FFIExample

import System.FFI

-- System info helpers

export
%foreign "C:int_size_bytes,shim"
prim_int_size_bytes : Int

bigs

module Libgit.Git

import Control.Monad.Reader

||| An abstract token representing the initialized libgit2 state. Its
||| constructor is purposefully not exported, a context can only be created
||| via `runGitT`.
export
data GitContext : (i : Type) -> Type where
  MkGitContext : GitContext i

bigs

module Adder

AdderType : Nat -> Type
AdderType 0 = Int
AdderType (S k) = Int -> AdderType k

adder : {n : Nat} -> {default 0 acc : Int} -> AdderType n
adder {n=Z} {acc} = acc
adder {n=S k} {acc} = \x => adder {n=k} {acc=acc + x}

bigs

module IndexedTypes

data Foo i = MkFoo
data FooInt i = MkFooInt Integer

mkFooInt : Foo i -> Integer -> FooInt i
mkFooInt _ = MkFooInt

addFoos : Foo i -> FooInt i -> FooInt i -> FooInt i
addFoos f (MkFooInt x) (MkFooInt y) = mkFooInt f (x + y)

bigs

module Data.Matrix

Matrix : (m: Nat) -> (n: Nat) -> (a: Type) -> Type
Matrix m n a = Vect m (Vect n a)

madd : Num a => {n : _} -> Matrix m n a -> Matrix m n a -> Matrix m n a
madd [] [] = []
madd (x :: xs) (y :: ys) = vadd {n=n} x y :: madd xs ys
  where
    vadd : {n : _} -> Vect n a -> Vect n a -> Vect n a

bigs

#!/bin/bash ruby

require "open3"

sigint_caught = false
Signal.trap("INT") do
  sigint_caught = true
  throw :sigint
end

bigs

Cole Brown

SPJ recently gave a fantastic talk on Edward Kmett's wildly useful lens library. Simon,a brilliant programmer and one of Haskell's designers, had little to no experience with lens prior to this talk and, resultingly, is able to offer a shockingly fresh perspective.

In his talk, he walks the audience through his deconstruction of the library — an illuminating journey. There is a lot of insight exposed, but there was one (perhaps unspoken) sentiment that struck me:

Functional programmers tend to prefer simple, versatile data structures like lists and trees. The reasoning is often times simple: simple data types yield powerful abstractions. One can implement a mind-boggling number of algorithms using maps and folds over lists (and associative lists).

While Haskell caters to this simplified model of programming, Haskell's type system and record syntax also encourage the use of abstract data ty