Andrey Mokhov snowleopard

I had a fun refactoring example in Haskell today I wanted to share. So, I've got a structure with a nested Maybe inside, which looked like this:

Maybe (Vector.Vector (Maybe (Direction, [Departure])))

I wanted to get that second-level Maybe folded into the first as it didn't provide any semantic meaning. So I start by writing the type definition:

	-- See also https://gist.github.com/copumpkin/2636229
	module Relations where

	open import Level
	open import Function
	open import Algebra
	open import Data.Empty
	open import Data.Sum as Sum
	open import Data.Product as Prod
	open import Relation.Binary

	{-# LANGUAGE DeriveFunctor #-}
	{-# LANGUAGE LambdaCase #-}

	import Control.Applicative.Free
	import Control.Monad
	import Control.Monad.Free
	import Control.Monad.Primitive
	import System.Random.MWC.Probability (Prob)
	import qualified System.Random.MWC.Probability as MWC

	Definition associative {A:Type} (op: A -> A -> A) :=
	forall x y z, op x (op y z) = op (op x y) z.

	Definition commutative {A:Type} (op: A -> A -> A) :=
	forall x y, op x y = op y x.

	Definition is_unit_left {A:Type} (op: A -> A -> A) one :=
	forall x, op one x = x.

	Definition is_unit_right {A:Type} (op: A -> A -> A) one :=

	{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs,
	ScopedTypeVariables, TypeOperators #-}

	-- \| Type-level natural numbers and singletons, with proofs of
	-- a few basic properties.

	module BasicNat (
	-- \| Type-level natural numbers
	Nat (..)
	, type (+)

	{-# LANGUAGE Rank2Types, FunctionalDependencies, FlexibleInstances #-}
	import Control.Monad (liftM, ap)
	import qualified Data.Set as S

	newtype SM a = SM {fromSM :: forall r. SetM a r => r}

	class SetM a r \| r -> a where
	{-Instances of 'SetM' must satisfy the following laws:

	* @'fromSet' s = 'fromList' $ 'Data.Set.toList' s@

	main = do
	let buildDir = "_build"
	-- how to express on a non-string level that everything should only ever be put into "_build"?
	-- how to never repeat that information anywhere else, much less do problematic string operations
	-- with the `"_build"` constant?
	staticDir = "static"
	staticFiles = map (staticDir <>) [ "foo" "bar" "baz" ]

	(buildDir </> staticDir </> "*") %> \outFile ->
	-- we only get `out`, which is some unknown string

	# A simple type system to check plain nix values
	# and get detailed error messages on type mismatch.
	#
	# Contains support for
	# scalars (simple values)
	# recursive types (lists of t and attrs of t)
	# products (attribute sets with named fields)
	# sums (tagged unions where you can match on the different cases)
	# unions (untagged unions of the specified types)
	# We can’t type functions (lambda expressions). Maybe in the future.

	import Numeric.Natural (Natural)

	import qualified Data.Semigroup

	-- \| @fibonacci n@ computes the @nth@ fibonacci number efficiently using infinite
	-- precision integer arithmetic
	--
	-- Try @fibonacci 1000000@
	fibonacci :: Natural -> Natural
	fibonacci n = x01 (Data.Semigroup.mtimesDefault n m)