Gurkenglas

Require Import ZArith.
Open Scope Z_scope.

Notation "x '/<' y" := (x / y)
  (at level 40, left associativity).

Definition div_nearest_down (x y : Z) : Z := (1 + (2 * x - 1) /< y) /< 2.

Notation "x '/~<' y" := (div_nearest_down x y)
  (at level 40, left associativity).

Gurkenglas

A tool can do no more than the tools it was defined from. Therefore, we might better predict it, and cache new insights.

Therefore, apply that tool when you can, so the reader needs not rederive those insights.

A tool is never longer than its definition. Therefore, it's a good heuristic to shorten your code.

The same goes for text, but then the reader needs definitions, hence the link to this post.

Recursion is the maximally powerful tool of pure code. Its irreducible use is surprisingly rare in practice.

Gurkenglas

{-# Language LambdaCase #-}
{-
  Functionality: 
    - Read all folders and sub-folders with structure like below
    - store all folder and file info in State monad, 
    - at the end of the loop, print it.
    ├── aaa
    │   ├── b
    │   │   ├── b1
    │   │   │   ├── b1-1

Gurkenglas

Microsoft Windows [Version 10.0.14393]
(c) 2016 Microsoft Corporation. Alle Rechte vorbehalten.

C:\Users\Gurkenglas>stack install ghci-ng
ghci-ng-10.0.0: configure
ghci-ng-10.0.0: build

--  While building package ghci-ng-10.0.0 using:
      C:\Users\Gurkenglas\AppData\Roaming\stack\setup-exe-cache\x86_64-windows\Cabal-simple_Z6RU0evB_1.24.0.0_ghc-7.10.3.exe --builddir=.stack-work\dist\b7fec021 build --ghc-options " -ddump-hi -ddump-to-file"
    Process exited with code: ExitFailure 1

Gurkenglas

Today I shall attack the problem of implementing subsequences :: [a] -> [[a]].

I'll be recounting my thought process like I'd imagine it to be if I was a little closer in smartness to where I wish I was.

Someone on #haskell just posted some way to implement it using lets and wheres and callbacks and one-character names and more, and that problem doesn't sound so hard, so I'll try implementing it myself.

Okay, how? Each element of the sequence needs to be in half the subsequences, and not in the other half. This reminds me of the monad of nondeterminism (also called [] monad) and using it with filterM:

<Gurkenglas> :t filterM (const [True, False])
<lambdabot> [b] -> [[b]]