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
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE GADTs #-} | |
module PlusZero where | |
import Data.Type.Equality | |
data Nat | |
= Zero |
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 Main where | |
import Prelude | |
import Control.Monad.Eff | |
import Control.Monad.Eff.Console | |
import Debug.Trace | |
import Data.Maybe |
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
{-# LANGUAGE NPlusKPatterns #-} | |
module Main where | |
import Test.QuickCheck | |
data NatF a | |
= ZeroF | |
| SuccF a | |
instance Functor NatF where |
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
// Whenever I complain about == in JS people always tell me | |
// that I should use ===, as if that would make more sense. | |
// the `sel` function takes three values of type A | |
// we know nothing about, therefore we should not | |
// be able to compute anything with these values, | |
// the only thing we should be able to do is | |
// to constantly return one of them, their | |
// value should not be able to influence the | |
// result in any way. |
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
{-# LANGUAGE LambdaCase #-} | |
module Main where | |
import Control.Applicative (liftA2) | |
import Control.Monad.Reader | |
type Varname = String | |
type Env = [(Varname, Dom)] | |
data Dom |
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
#!/usr/bin/env runhaskell | |
-- run as script to get correct buffering behavior | |
-- >>> chmod +x ./script.hs | |
-- >>> ./script.hs | |
module Main where | |
import Control.Exception | |
example :: IO Int | |
example = |
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 -O2 #-} | |
{-# LANGUAGE OverloadedStrings #-} | |
module Main where | |
import System.IO | |
import Text.Regex.PCRE | |
import Text.Regex.PCRE.ByteString.Lazy | |
import Data.Maybe (mapMaybe) | |
import Data.Char (ord) | |
import Data.Word (Word8) |
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 Main where | |
import Data.Foldable (traverse_) | |
import Text.Printf | |
printThat x = do | |
printf "Now printing %d elements\n" (length x) | |
traverse_ putStrLn x | |
main = do |
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
{-# LANGUAGE DeriveFunctor #-} | |
{-# LANGUAGE GeneralizedNewtypeDeriving #-} | |
{-# LANGUAGE LambdaCase #-} | |
module Main where | |
import Control.Monad.Trans.Free | |
import Control.Monad.State | |
import Control.Monad.IO.Class (liftIO) | |
import System.IO (hFlush, stdout) |
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 Main | |
data Free : (f : Type -> Type) -> (a : Type) -> Type where | |
Pure : a -> Free f a | |
Bind : f (Free f a) -> Free f a | |
instance Functor f => Functor (Free f) where | |
map f (Pure x) = Pure (f x) | |
map f (Bind x) = assert_total (Bind (map (map f) x)) |