This file contains 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
-------------------------------------------------------------------------------- | |
-- Is List or NonEmpty "simpler"? Neither: | |
type NonEmpty a = Fix (Compose ((,) a) Maybe) | |
type List a = Fix (Compose Maybe ((,) a)) | |
-------------------------------------------------------------------------------- | |
newtype Fix f = Fix {unFix :: f (Fix f)} |
This file contains 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/chrislpenner/status/1221784005156036608 | |
-- | |
-- The goal is to mimic this Scala code, but in Haskell: | |
-- | |
-- > "spotify:user:123:playlist:456" match { | |
-- > case s"spotify:user:$userId:playlist:$playlistId" | |
-- > => ($userId, $playlistId) // ("123", "456") | |
-- > } | |
{-# LANGUAGE DeriveFunctor, LambdaCase, PatternSynonyms, QuasiQuotes, RankNTypes, TemplateHaskell, TypeOperators, ViewPatterns #-} | |
{-# OPTIONS -Wno-name-shadowing #-} |
This file contains 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
module Spec where | |
import Quickstrom | |
import Data.Foldable (any) | |
import Data.Maybe (maybe) | |
import Data.Tuple (Tuple(..)) | |
import Data.String.CodeUnits (contains) | |
import Data.String.Pattern (Pattern(..)) | |
readyWhen = "body" |
This file contains 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
{-# OPTIONS_GHC -fno-warn-orphans #-} | |
module Repl where | |
import Cachix.Config (readConfig) | |
import Cachix.Env (setupApp) | |
import Cachix.Server.Prelude | |
import qualified Control.Exception.Safe as Safe | |
import qualified Language.Haskell.Interpreter as Interpreter | |
import Protolude |
This file contains 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
module FoldsAndUnfolds where | |
import Data.List -- for unfoldr | |
class Functor f => Recursive f t | t -> f where | |
project :: t -> f t | |
cata :: (f a -> a) -> t -> a | |
cata alg = go where go = alg . fmap go . project |
This file contains 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
-- https://icfp21.sigplan.org/details/icfp-2021-papers/21/Calculating-Dependently-Typed-Compilers-Functional-Pearl- | |
{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies, TypeApplications, KindSignatures, ScopedTypeVariables #-} | |
import Control.Applicative | |
import Data.Kind | |
import Data.Type.Equality | |
type family (a :: Bool) || (b :: Bool) :: Bool where | |
'False || b = b | |
'True || b = 'True |
This file contains 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
/- | |
A proof of the correctness of an arithmetic expression compiler in Lean 4. | |
Ported from [expcompile.v], which is part of Derek Dreyer and Gert Smolka's | |
[course material]. | |
[expcompile.v]: https://www.ps.uni-saarland.de/courses/sem-ws17/expcompile.v | |
[course material]: https://courses.ps.uni-saarland.de/sem_ws1718/3/Resources | |
-/ |
This file contains 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
// Faster solution for: | |
// http://www.boyter.org/2017/03/golang-solution-faster-equivalent-java-solution/ | |
// With threading. | |
// g++ -std=c++11 -Wall -Wextra -O3 -pthread | |
// On my computer (i5-6600K 3.50 GHz 4 cores), takes about ~160 ms after the CPU | |
// has warmed up, or ~80 ms if the CPU is cold (due to Turbo Boost). | |
// How it works: Start by generating a list of losing states -- states where the | |
// game can end in one turn. Generate a new list of states by running the game |
This file contains 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
(** {0 Elaboration with Record Patching and Singleton Types} | |
This is a small implementation of a dependently typed language with | |
dependent record types, with some additional features intended to make it | |
more convenient to use records as first-class modules. It was originally | |
ported from {{: https://gist.github.com/mb64/04315edd1a8b1b2c2e5bd38071ff66b5} | |
a gist by mb64}. | |
The type system is implemented in terms of an ‘elaborator’, which type | |
checks and tanslates a user-friendly surface language into a simpler and |
This file contains 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
## Principal type-schemes for functional programs | |
**Luis Damas and Robin Milner, POPL '82** | |
> module W where | |
> import Data.List | |
> import Data.Maybe | |
> import Data.Function |
OlderNewer