gelisam

-- in response to https://twitter.com/_julesh_/status/1573281637378527232
--
-- The challenge is to implement a partial function of type
--
--     list :: [Lens s t a b]
--          -> Lens [s] [t] [a] [b]
--
-- while using the existential representation of lenses.
{-# LANGUAGE GADTs, ScopedTypeVariables #-}

gelisam

-- In response to https://twitter.com/totbwf/status/1565154284135534592?s=20&t=1rtY9RMVImoAopR-ia24zA
{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeApplications #-}
module Main where

import Prelude hiding (head, tail)
import Test.DocTest (doctest)

-- $setup
-- >>> import System.Timeout (timeout)

gelisam

-- from https://twitter.com/haskell_cat/status/1533795075154755584
--
-- a micro-benchmark confirming that forcing the head of
--   ((xs_0 ++ xs_1) ++ ...) ++ xs_n
-- only takes linear time even though forcing the whole thing would
-- take quadratic time. It sure looks quadratic between n=1000 and
-- n=16000 though!

{-# LANGUAGE BangPatterns #-}
module Main where

gelisam

-- | In response to https://twitter.com/_gilmi/status/1478846678409035779
--
-- The challenge is three-fold:
--
-- 1.  define the type 'Expr2' as "the same as 'Expr1' but with this constructor
--     instead of that one", without having to repeat all the other constructors.
-- 2.  convert from 'Expr1' to 'Expr2' by only providing a translation for the
--     one constructor which is different.
-- 3.  write a polymorphic function which works with both 'Expr1' and 'Expr2'
--     because it doesn't touch the constructor which differs.

gelisam

-- in response to https://twitter.com/BartoszMilewski/status/1466106578524786690
-- 
-- Can we solve https://adventofcode.com/2021/day/1 using the NonEmpty Comonad?
{-# LANGUAGE LambdaCase, ScopedTypeVariables #-}
import Prelude hiding (sum)
import Control.Category ((>>>))
import Control.Comonad (Comonad(extract, extend))
import Control.Monad (guard)
import Data.Either (rights)
import Data.List.NonEmpty (NonEmpty((:|)))

gelisam

-- In response to https://twitter.com/mattoflambda/status/1430314500285214725,
-- more specifically the "It could be a row type, like PureScript. That’d be
-- awesome" bit. We do have row types in Haskell, they just come as a library
-- instead of being built into the language! Here's my solution using vinyl and
-- composite.
{-# LANGUAGE DataKinds, FlexibleContexts, TemplateHaskell, TypeApplications, TypeOperators #-}
module Main where

import Control.Lens
import Composite.Record (type (:->), Record, val)

gelisam

-- Yet another technique for generating proofs in Agda (in addition to the ones
-- I've described in https://gist.github.com/gelisam/486d4992c0f3a3f3da2f58ff0e1a3e72):
-- transform the proposition into a simpler one which can be proved using refl.
--
-- This is the approach I use in my https://github.com/agda/agda-finite-prover
-- package, which can prove equations universally-quantified over finite types,
-- e.g. proving the commutativity of the boolean function '∧'. I simplify the
-- proposition to a long enumeration of all the concrete cases, each of which
-- can be proved using refl:
--

gelisam

-- In response to https://www.reddit.com/r/haskell/comments/lu14nu/is_it_possible_to_get_a_repl_in_a_state_monad/
--
-- The challenge is to write a repl in which we can run State effects in
-- addition to ghci's basic features of binding variables, inspecting values,
-- and running IO effects.
--
-- Well, the original request was whether it was possible to somehow add those
-- features to ghci. But being the maintainer of the hint library, I thought I
-- should demonstrate how easy it is to write your own ghci alternative which
-- has those features built-in!

gelisam

-- inspired by this twitter conversation: https://twitter.com/haskell_cat/status/1360005114430390279
-- 
-- summary:
--   * by hand is fastest, then with a getter/setter pair, then van Laarhoven, then profunctor optics.
--   * in every representation, ghc can optimize 'view' to be as fast as doing it by hand
--   * there are no representations in which ghc can similarly optimize 'set' or 'modify'
--
-- criterion report: http://gelisam.com/files/lens-benchmark/benchmark.html

{-# LANGUAGE RankNTypes, TupleSections #-}

gelisam

-- A demonstration of Agda's mechanisms for generating proofs:
-- * 1. fromMaybe
-- * 2a. macros
-- * 2b. type-aware macros
-- * 2c. stuck macros
--
-- Tested using Agda-2.6.1.1 and agda-stdlib-1.4

module GeneratingCode where