gelisam

-- The challenge posed by @sellout on the Monoidal Café
-- (https://discord.com/channels/1005220974523846678/1153280045679390770/1374915124925825104)
-- is to implement a version of histo which supports types which
-- are isomorphic to Cofree without requiring a Corecursive instance on that type.
--
-- The Monoidal Café is a private Discord server, so here is the text of the
-- challenge if you don't have access:
--
-- > So, IIRC, for `histo = gcata distHisto`,  you can generalize from `Cofree`
-- > to an arbitrary `Corecursive (cofreef a) (EnvT a f)`, in which case

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

#!/usr/bin/env stack
-- stack --resolver lts-8.16 script

-- for https://www.reddit.com/r/haskell/comments/6emo9g/trying_to_get_the_basic_example_in_cloudhaskell/
{-# LANGUAGE LambdaCase, RecordWildCards #-}
import System.Environment (getArgs)
import Control.Distributed.Process
import Control.Distributed.Process.Node (initRemoteTable)

import Control.Distributed.Process.Backend.SimpleLocalnet

gelisam

-- in reply to http://www.reddit.com/r/haskell/comments/21mja6/make_lllegal_state_transitions_unrepresentable/
-- 
-- We implement a tiny language with three commands: Open, Close, and Get.
-- The first Get after an Open returns 1, the second Get returns 2, and so on.
-- 
-- Get is only valid while the state is open, and
-- Open must always be matched by a Close.
-- We enforce both restrictions via the type system.
-- 
-- There are two valid states: Opened and Closed.

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

{-# OPTIONS --copatterns #-}
module Main where
-- A simple cat program which echoes stdin back to stdout, but implemented using copatterns
-- instead of musical notation, as requested by Miëtek Bak (https://twitter.com/mietek/status/806314271747481600).

open import Data.Nat

open import Data.Unit
open import Data.Bool
open import Data.Char

gelisam

-- A concrete use case for the type which is to '(->)' as 'Day' is to '(,)'.
-- I call it "FunDay", but I don't know what its proper name is. I've been
-- trying to find a use for 'FunDay', and I think I've found a pretty neat one.

{-# LANGUAGE FlexibleContexts, FlexibleInstances, PolyKinds, RankNTypes, TypeSynonymInstances #-}
module Main where
import Test.DocTest

import Control.Monad.Except
import Control.Monad.Reader

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