Skip to content

Instantly share code, notes, and snippets.

Alex Beal beala

Block or report user

Report or block beala

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
beala / Config
Last active Dec 16, 2017
Use Dhall ( and dhall-text ( to generate a training script for tensorflow training.
View Config
-- Type decl for parameters to the training script.
{ architecture : Text
, learningRate : List Double
, steps : List Natural
, unknownPercent : Natural
, windowStrideMs : Natural
, startingCheckpoint: Optional Natural

Yosemite Valley Sep 3d 1843

Dear Sister Sarah,

I have just returned from the longest & hardest trip I have ever made in the mtns., having been gone over five weeks. I am weary but resting fast, Sleepy but sleeping deep & fast, hungry but eating much – For two weeks I explored the glaciers of the summits east of here, sleeping among the snowy mtns without blankets & with but little to eat on account of its being so inaccessible. After my icy experiences it seems strange to be down here in so warm & flowery a climate.

I will soon be off again determined to use all the season in prosecuting my researches — will go next to Kings river a hundred miles south, then to Lake Tahoe & adjacent mtns. & in winter work in Oakland with my pen. The Scotch are slow but some day I will have the results of my mountain studies in a form in which you all will be able to read & judge of them. In the mean time I write occaisonally for the Overland Monthly but neither these magazine articles nor my first book will form any fini

beala / TreeRotation.idr
Created Mar 5, 2017
Proving some properties of binary trees and rotation in idris.
View TreeRotation.idr
In this file I:
- Define a binary tree.
- Define a type level predicate for right rotation of a tree. That is, this type
can only be instantiated for trees that can be right rotated.
- Prove that it's decidable if a tree can be right-rotated or not.
- Prove that right-rotating a tree preserves in-order traversal.
-- A binary tree.
beala / ¯|_(ツ)_|¯.scala
Created Jun 17, 2016
I've been using Scala for years and I have no idea how inheritance works.
View ¯|_(ツ)_|¯.scala
class C {
val a: Int = 1
val b: Int = a + 10
class B extends C {
override val a: Int = 100
println(s"a = ${new B().a}")
beala / Cryptol.agda
Last active Jun 14, 2016
A runnable implementation of the "Cryptol view" from the "Power of Pi": I also attempted to implement part of SHA-1.
View Cryptol.agda
open import Data.Vec hiding (take; drop; [_]; split)
open import Data.Nat using (_*_; ℕ; zero; suc; _+_)
open import Data.Fin using (Fin; _≤_; compare; toℕ)
open import Relation.Binary.Core using (_≡_; refl)
open import Relation.Binary.PropositionalEquality using (cong)
import Data.Bool.Base as B using (if_then_else_; Bool; _∧_; true; false)
-- A runnable implementation of the "Cryptol View" from "The Power of Pi"
-- by Nicolas Oury and Wouter Swierstra with an implementation of SHA-1
beala / TabsVsSpaces.scala
Last active May 31, 2016
Mixing tabs and spaces is great... in theory.
View TabsVsSpaces.scala
// Indent with tabs (␉), align with spaces (␠)
class C {
def f(loooooooooooooooooooooooongName: String
␉ ␠␠␠␠␠␠b: String): Unit = {
␉ ␉ doThing(loooooooooooooooooooooooongName,
␉ ␉ ␠␠␠␠␠␠␠␠b)
␉ }
beala /
Last active May 29, 2016
Some thoughts on Agda (and I suppose dependent types in general) after a few days of exploring.

I've been using Agda for less than a week now, so I want to avoid making too many grand statements about it, but so far my impression is that the increase in power over, say, Haskell is large. It feels similar to the increase in power that one gets from moving from a language that doesn't support FP to a language that does. For example, I can try to program functionally in JavaScript, but it's not clear there's much benefit to it, and there may even be harm (try keeping a monad transformer stack straight without compiler support, and then discovering the inevitable bugs at run time). Moving to Haskell, it becomes clear how the generality baked into FP abstractions helps me use the type system to its fullest.

In Haskell, we like to talk about the benefits of equational reasoning, but I think it's rare that practitioners actually get out their pens and paper and write proofs [1]. Instead, the benefit is that enforcing the constraints that make equational reasoning possible makes informal reasoning easier. It

beala / Nats.agda
Last active Mar 20, 2019
Some proofs of basic properties of addition and equality in Agda. Update: Now lists and multiplication!
View Nats.agda
module Nats where
open import Agda.Primitive
data Equal {a : Level} {X : Set a} : X → X → Set a where
equal : {x : X} Equal x x
_==_ : _
_==_ = Equal
View memoFibs.scala
val memoFib: Int => Int = {
case 0 => 0
case 1 => 1
case n => memoFib(n-2) + memoFib(n-1)
View etaFibs.hs
-- Eta expanded
slow :: Int -> Integer
slow i = (fmap fibs [0 ..] !! i)
fibs 0 = 0
fibs 1 = 1
fibs n = slow (n-2) + slow (n-1)
-- Eta reduced
fast :: Int -> Integer
You can’t perform that action at this time.