chrisdone

-- λ> eval (A (L (\(C i) -> C (i * 2))) (C 2))
-- 4

{-# LANGUAGE GADTs #-}

data E a where
  C :: a -> E a
  L :: (E a -> E b) -> E (a -> b)
  A :: E (a -> b) -> E a -> E b

rampion

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

rossdylan

module Main where
import System.ZMQ
import Control.Monad (replicateM, forever)
import qualified Data.ByteString
import Text.Printf

type Topics = [String]
type MessageHandler = (Data.ByteString.ByteString -> IO ())

subscribeTopics :: SubsType a => Topics -> Socket a -> IO ()

andrejbauer

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.

puffnfresh

Inductive bool : Type :=
  | true : bool
  | false : bool.

Class Monoid (A : Type) :=
  {
    empty : A ;
    append : A -> A -> A ;

    left_neutrality : forall x, append empty x = x ;

puffnfresh

module AlaCarte where

-- Control.Monad.Free

data Free f a = Free (f (Free f a)) | Pure a

instance Functor f => Monad (Free f) where
    Pure a >>= f = f a
    Free r >>= f = Free (fmap (>>= f) r)
    return = Pure

AndrasKovacs

{-
    Copyright (C) 2014 András Kovács

    Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

    The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOF

relrod

Unpackaged ghc-lens deps:


BuildRequires:  ghc-bifunctors-devel       #
BuildRequires:  ghc-comonad-devel          #
BuildRequires:  ghc-contravariant-devel    #1075598
BuildRequires:  ghc-distributive-devel     #1075605
BuildRequires:  ghc-exceptions-devel       #1075601
BuildRequires:  ghc-profunctors-devel      #
BuildRequires:  ghc-reflection-devel       #1076737

darkf

import Data.Maybe (fromJust)

data Type = IntTy
		  | ArrowTy Type Type
	deriving (Show, Eq)

data Term = Const Int
		  | Var String
		  | Abs String Type Term
		  | App Term Term

puffnfresh

Scala Lenz

This library is a port of Haskell's lens. The goal is to provide functional lenses, isomorphisms, getters and setters.

Examples

Isomorphisms