kosmikus

{-# 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

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

{-# 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

kosmikus

{-# 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

kosmikus

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

{-# 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

{-# 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

kosmikus

<root>
|- greet
|  v
|  `-*
|  v
|  `- <dyn>
|     `-*
`- hello
   `- <dyn>
      `-*

kosmikus

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:

kosmikus

{-# 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