gelisam

-- a demonstration that a function can be passed a postulate as an irrelevant
-- argument and still still compute a result
module Irrelevance where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

gelisam

open import Data.List using (List; _∷_; [])
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Show renaming (show to showℕ)
open import Data.String
open import Relation.Binary.PropositionalEquality

{-# NO_POSITIVITY_CHECK #-}
data FixI {Index : Set} (f : (Index → Set) → (Index → Set)) (i : Index) : Set where
  InI

gelisam

-- In response to https://twitter.com/kmett/status/1738168271357026634
--
-- The challenge is to implement a version of
--
-- > mapKeys :: Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
--
-- which costs O(1) if the (k1 -> k2) function is coerce and the coercion
-- preserves the ordering, O(n) if the function is injective, and O(n log n)
-- otherwise. Obviously, the implementation can't inspect a pure function in
-- order to determine which case it is, so our version will need to use a

gelisam

{-# LANGUAGE KindSignatures, GADTs, RankNTypes, ScopedTypeVariables #-}
module Main where

import Prelude hiding (id, (.))

import Control.Arrow
import Control.Category
import Data.Kind (Type)
import Data.Function ((&))
import Data.Profunctor

gelisam

-- A proof of concept for a value-based debugging technique: instead of
-- debugging by imperatively stepping through the evaluation, we instead
-- produce a value representing the evaluation tree.
--
-- This value can then be manipulated like any other value, e.g. instead adding
-- a breakpoint and stepping until the breakpoint is hit, you can write an
-- ordinary function which recurs into the evaluation tree until it finds a node
-- of interest. This way, more complex conditions can be easily expressed, e.g.
-- "find the smallest subtree in which a call of 'double' does not result in an
-- output which is the double of its input".

gelisam

-- Defining a custom recursion scheme to manipulate two mutually-recursive
-- types, in the context of a toy bidirectional type checker.
{-# LANGUAGE DerivingStrategies, GeneralizedNewtypeDeriving, ScopedTypeVariables #-}
module Main where

import Test.DocTest

import Control.Monad (when)
import Data.Bifunctor (Bifunctor(bimap))
import Data.Bifoldable (Bifoldable(bifoldMap), bitraverse_)

gelisam

-- Follow up to [1], praising @viercc's better solution [2].
--
-- [1] https://gist.github.com/gelisam/a8bee217410b74f030c21f782de23d11
-- [2] https://www.reddit.com/r/haskell/comments/yb9bi4/comment/itfh07z
--
-- The challenge is still to implement a function which takes in three
-- Conduits, and uses the values from the first Conduit in order to decide
-- which of the other two Conduits to sample from next. Something like this:
--
--     example bools ints strings = do

gelisam

-- in response to https://www.reddit.com/r/haskell/comments/yb9bi4/using_multiple_conduits_as_input_streams/
--
-- The challenge is to implement a function which takes in
-- three Conduits, and uses the values from the first
-- Conduit in order to decide which of the other two
-- Conduits to sample from next. Something like this:
--
--     example bools ints strings = do
--       maybeBool <- awaitMaybe bools
--       case maybeBool of

gelisam

-- Based on https://gist.github.com/jship/d2237fad40cfb34166d82597735fbacf
--
-- The above example demonstrates how to flatten all the routes in a record of
-- records of routes, in order to bind a long list of top-level 'Link'
-- functions.
--
-- Below, I demonstrate how to instead go from a record of records of routes to
-- a record of records of 'Link's, and how to easily navigate the resulting
-- nested record.
{-# LANGUAGE DataKinds, DeriveGeneric, DerivingStrategies, FlexibleContexts, GADTs, TypeApplications, TypeOperators #-}

gelisam

-- in response to https://twitter.com/sjoerd_visscher/status/1574390090406989824
--
-- The challenge is to implement a partial function of type
--
--     list :: Traversable f
--          => f (Lens s t a b)
--          -> Lens (f s) (f t) (f a) (f b)
--
-- using the existential representation of lenses.
--