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 OverloadedLabels #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE InstanceSigs #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE AllowAmbiguousTypes #-} | |
import GHC.OverloadedLabels | |
import GHC.TypeLits | |
import Data.Proxy | |
import GHC.Records |
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 --no-unicode #-} | |
module BV where | |
data Two : Set where | |
ff tt : Two | |
data BV : Set where | |
end : BV | |
_-,_ : BV -> Two -> BV |
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 Bla where | |
-- declare constants to minimise example | |
-- just assume Set == Type | |
postulate | |
-- there is a type called String | |
String : Set | |
-- it has a value called 'hey' in it | |
hey : String | |
-- there is a type called Int |
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 RankNTypes #-} | |
import Control.Monad (replicateM_, when) | |
import Control.Monad.Primitive (PrimMonad, PrimState) | |
import qualified Data.Vector as V | |
import qualified Data.Vector.Mutable as M | |
import System.Random (StdGen, newStdGen, randomR) | |
import Data.Traversable (for) | |
import Data.Functor (void) | |
import Control.Monad.Trans.State.Strict (put, execStateT, get, gets) |
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 #-} | |
import Control.Monad.Trans.Reader (runReader, local, ask, Reader) | |
import Data.Maybe (mapMaybe) | |
data Paren = LParen | RParen | |
balanced :: [Paren] -> Bool | |
balanced xs = flip runReader 0 $ go xs | |
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
{-# LANGUAGE EmptyCase #-} | |
{-# LANGUAGE LambdaCase #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE GADTs #-} | |
import Data.Kind (Type) | |
data Tree a | |
= Empty |
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 BlockArguments #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE StandaloneDeriving #-} | |
{-# LANGUAGE TypeApplications #-} | |
{-# LANGUAGE TypeOperators #-} | |
import Data.Bitraversable (bisequence) |
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 FlexibleInstances #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE InstanceSigs #-} | |
class ApplyCompose b c x res | b c x -> res where | |
(<|) :: (b -> c) -> x -> res | |
instance ApplyCompose b c (a -> b) (a -> c) where | |
(<|) :: (b -> c) -> (a -> b) -> a -> c | |
(<|) = (.) |
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 AllowAmbiguousTypes #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE TypeFamilies #-} | |
type family Ambiguous (a :: k) :: b where | |
Ambiguous x = x | |
all' :: Foldable (Ambiguous t) => (a -> Bool) -> Ambiguous t a -> Bool | |
all' = all |
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 AllowAmbiguousTypes #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE TypeFamilies #-} | |
type family Ambiguous (a :: k) :: b where | |
Ambiguous x = x | |
toInteger' :: Integral (Ambiguous a) => Ambiguous a -> Integer | |
toInteger' = toInteger |
NewerOlder