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)
@kosmikus
kosmikus / TinyServant.hs
Created November 1, 2015 20:30
Implementation of a small Servant-like DSL
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators #-}
{-# LANGUAGE TypeFamilies, FlexibleInstances, ScopedTypeVariables #-}
{-# LANGUAGE InstanceSigs #-}
module TinyServant where
import Control.Applicative
import GHC.TypeLits
import Text.Read
import Data.Time
{-# 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