Skip to content

Instantly share code, notes, and snippets.

{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
module FirstField where
import Generics.SOP
class HasHead (y :: *) (xs :: [*]) where
hhead :: NP I xs -> K y xs
instance (x ~ y) => HasHead y (x ': xs) where
@kosmikus
kosmikus / FoldMutRec.hs
Last active October 13, 2015 11:02
Two examples of Foldable for mutually recursive datatypes
module FoldMutRec where
-- Note: DeriveFoldable could be used, but I am providing
-- hand-written instances to better illustrate the mechanics.
import Data.Monoid
data Forest a = Forest [Tree a]
data Tree a = Node a (Forest a)
{-# LANGUAGE DeriveGeneric, FlexibleInstances, ScopedTypeVariables, FlexibleContexts, DataKinds, TypeFamilies #-}
module SwaggerExample where
import Data.Proxy
import qualified GHC.Generics as G
import Generics.SOP
data Todo = Todo {
created :: Int
, description :: String
module FromInteger
import Data.Vect
-- This is inspired by the fromInteger definition for Fin.
IntegerToElem :
DecEq a => (i : Integer) -> (x : a) -> (xs : Vect n a)
-> Maybe (Elem x xs)
IntegerToElem i x [] = Nothing
@kosmikus
kosmikus / Fold.hs
Created December 3, 2015 08:09
Regensburg Haskell Meetup December 2015
{-# LANGUAGE GADTs, InstanceSigs, TypeFamilies #-}
{-# LANGUAGE FlexibleContexts, RankNTypes, PatternSynonyms #-}
module Fold where
import Prelude hiding (foldr, take, all)
---------------------------------------------------------------------------
-- "foldr" on lists, Maybe, Bool, and binary trees
---------------------------------------------------------------------------
@kosmikus
kosmikus / TypeError.hs
Created January 9, 2016 16:33
Strange TypeError behaviour
{-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
import GHC.TypeLits (TypeError, ErrorMessage(..))
type family Resolve (t :: Type -> Type) :: Type -> Type where
Resolve _ = TypeError (Text "ERROR")
-- testOK :: Resolve [] Int
<root>
|- greet
| v
| `-*
| v
| `- <dyn>
| `-*
`- hello
`- <dyn>
`-*
type PermApi1 =
"a" :> "b" :> "c" :> Get '[JSON] ()
:<|> "b" :> "a" :> "c" :> Get '[JSON] ()
:<|> "a" :> "c" :> "b" :> Get '[JSON] ()
:<|> "c" :> "a" :> "b" :> Get '[JSON] ()
:<|> "b" :> "c" :> "a" :> Get '[JSON] ()
:<|> "c" :> "b" :> "a" :> Get '[JSON] ()
Output:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE OverloadedStrings #-}
module Main where
import Control.Applicative
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans.Either
@kosmikus
kosmikus / gist:c411abf4390dfd1adbcc16f6b665eb43
Created June 30, 2016 10:46
count-conflicts-2 on universe
[ghc-7.0.4-plain] andres@neli:~/repos/universe (git:master) $ rm -rf dist-newstyle && ~/bin/cabal-cc2 new-configure --max-backjumps=-1 --dry-run +RTS -t
Resolving dependencies...
In order, the following would be built (use -v for more details):
base-orphans-0.5.4
binary-0.8.2.1
deepseq-1.3.0.2
Cabal-1.20.0.4
deepseq-1.4.2.0
bytestring-builder-0.10.8.1.0
stm-2.4.4.1