This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- in response to https://twitter.com/xgrommx/status/1574392204071575558 | |
-- | |
-- The challenge is to implement a partial function of type | |
-- | |
-- list :: [Lens s t a b] | |
-- -> Lens [s] [t] [a] [b] | |
-- | |
-- while using the profunctor representation of lenses. This is based on my | |
-- implementation [1] of the previous challenge [2]. | |
-- |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 #-} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- | 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. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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((:|))) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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: | |
-- |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 #-} |