beala

// Indent with tabs (␉), align with spaces (␠)
class C {
␉ def f(loooooooooooooooooooooooongName: String
␉ ␠␠␠␠␠␠b: String): Unit = {
␉ ␉ doThing(loooooooooooooooooooooooongName,
␉ ␉ ␠␠␠␠␠␠␠␠b)  
␉ }
}

beala

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

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
{-# BUILTIN EQUALITY Equal #-}

_==_ : _
_==_ = Equal

beala

val memoFib: Int => Int = {
  Stream.from(0).map{
      case 0 => 0
      case 1 => 1
      case n => memoFib(n-2) + memoFib(n-1)
    }
}

beala

-- Eta expanded
slow :: Int -> Integer
slow i = (fmap fibs [0 ..] !! i)
  where 
    fibs 0 = 0
    fibs 1 = 1
    fibs n = slow (n-2) + slow (n-1)
    
-- Eta reduced
fast :: Int -> Integer

beala

import Control.Monad.State.Strict
import qualified Data.Map.Strict as Map

-- This is the standard fibonacci implementation with exponential complexity.
naiveFibs :: Int -> Integer
naiveFibs 0 = 0
naiveFibs 1 = 1
naiveFibs n = naiveFibs (n-2) + naiveFibs (n-1)

-- For reference, calculating the 35th fibonacci takes 9.49 sec.

beala

import Control.Monad.Logic
import Control.Monad.Logic.Class
import Data.Foldable (msum, traverse_)
import Data.List (elem)

main :: IO ()
main = do
  let allSolutions = observeAll queens
  traverse_ (putStrLn . prettyBoard) allSolutions
  putStrLn ("Number of solutions: " ++ (show (length allSolutions))) 

beala

This is a write up of my experience implementing the Functor, Applicative and Monad instances for Cont for the first time. What's notable is I used typed holes to guide me. By simply responding to the types and ghci's feedback, I arrived at a correct implementation.

I start with the newtype for Cont (this is the only thing I looked up beforehand) and the beginning of a Functor instance. I know from the type of fmap that I'll need to produce a Cont r b, so I start with the Cont constructor and a lambda with a hole

newtype Cont r a = Cont {runCont :: (a -> r) -> r}

beala

{-# LANGUAGE DeriveFunctor #-}

module ConsoleT where

import Control.Monad.Trans.Free
import Control.Monad.IO.Class
import Control.Monad.Identity
import Control.Monad.Trans.Class

import Control.Applicative.Free

beala

{-# LANGUAGE DeriveFunctor, FlexibleContexts, TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables #-}

module ConsoleDsl where

-- This file explains one technique for interleaving custom Free eDSLs with
-- existing monad stacks. This article does not explain Free or monad
-- transformers from the ground up, so some familiarity is assumed.

-- I begin by sketching out a basic Free eDSL, which enables printing to and
-- reading from the console. I then show how the eDSL doesn't play well with other