Skip to content

Instantly share code, notes, and snippets.

View gallais's full-sized avatar

G. Allais gallais

View GitHub Profile
@gallais
gallais / Deriving.hs
Created November 25, 2024 15:00
Putting the FUN in Functors
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Deriving where
import Data.Kind (Type)
newtype Cst a i = MkCst { runCst :: a }
newtype Idt i = MkIdt { runIdt :: i }
newtype Prd k l i = MkPrd { runPrd :: (k i, l i) }
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
import Control.Concurrent (forkIO, MVar, newEmptyMVar, putMVar, takeMVar)
import Data.Kind (Type)
@gallais
gallais / ShaSearch.hs
Created November 19, 2024 17:05
Looking for self-referential sentences
module ShaSearch where
import System.Process (readProcess)
-----------------------------------------------
-- Using the list monad to generate all the
-- hexadecimal words of a given length
-- All the hexadecimal characters
hexa :: [Char]
@gallais
gallais / Rot13.hs
Last active December 6, 2023 10:15
Finding words that are their own rot13
module Rot13 where
import Control.Monad (guard)
import Data.Char (ord, chr, toLower, isLower)
import Data.Function (on)
import Data.List (sortBy)
import Data.Maybe (mapMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
@gallais
gallais / Error.idr
Created February 24, 2022 17:19
Error monad in CPS style
module Error
export
data Error : (err, a : Type) -> Type where
MkError : (forall r. (err -> r) -> (a -> r) -> r) -> Error err a
export %inline
runError : Error err a -> (err -> r) -> (a -> r) -> r
runError (MkError hdl) kE kV = hdl kE kV
module LambdaLetRec
import Data.List1
import Data.List.Quantifiers
--------------------------------------------------------------------------------
-- types
infixr 5 ~>
@gallais
gallais / ElemSplit.idr
Created September 30, 2021 10:16
Magic pattern-matching on `Elem`
import Data.String
import Data.List
import Data.List.Elem
import Decidable.Decidable
import Decidable.Equality
%default total
toWitness : (prf1 : Dec a) -> IsYes prf1 -> a
toWitness (Yes prf2) x = prf2
@gallais
gallais / Smaller.agda
Created August 2, 2020 14:52
Returning a smaller sized list
open import Agda.Builtin.Size
open import Data.Maybe.Base
data List {n} (T : Set n) (i : Size) : Set n where
[] : List T i
_∷_ : ∀ {j : Size< i} → T → List T j → List T i
data Smaller {n} (T : Size → Set n) (i : Size) : Set n where
[_] : {j : Size< i} → T j → Smaller T i
{-# OPTIONS --safe --without-K #-}
module SyntaxDesc (I : Set) where
open import Agda.Primitive using () renaming (Set to Type)
open import Data.Nat.Base
open import Data.Fin.Base
open import Data.List.Base using (List; []; _∷_; _++_)
data Desc : Type₀ where
@gallais
gallais / PalAcc.v
Created May 22, 2020 12:02
Palindrome via an accumulator-based definition.
Require Import List.
Inductive PalAcc {A : Type} (acc : list A) : list A -> Type
:= Even : PalAcc acc acc
| Odd : forall x, PalAcc acc (x :: acc)
| Step : forall x xs, PalAcc (x :: acc) xs -> PalAcc acc (x :: xs)
.
Definition Pal {A : Type} (xs : list A) : Type := PalAcc nil xs.