phadej

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
module Parts where

import Data.Kind

import Control.Applicative (liftA2)
import Data.Function

-- in blogs

phadej

module Staged where

open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- indices, we could open import Data.Fin renaming too.
-- probably should (so we get all the lemmas).
-- but for now it's defined inline.

phadej

Revision history for bug23034

0.1.0.0 -- YYYY-mm-dd

• First version. Released on an unsuspecting world.

phadej

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}

phadej

{-# LANGUAGE OverloadedStrings #-}

import Network.HTTP.Client
import Network.HTTP.Client.Internal (Connection, openSocketConnection, makeConnection)
import Network.Socket.ByteString (sendAll, recv)

import qualified Control.Exception as E
import qualified Network.Socket as NS

main :: IO ()

phadej

{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators, UndecidableInstances #-}

#if __GLASGOW_HASKELL__ < 708
#error "requires GHC 7.10 or newer"
#endif
module Main (main) where

phadej

-- Normalization by evaluation for λ→2
-- Thorsten Altenkirch and Tarmo Uustalu (FLOPS
--
-- Agda translation by Oleg Grenrus
-- no proofs yet.

module Lambda2 where

open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
import Data.Nat.Properties as ℕ

phadej

module Monotone where

open import Data.Nat using (ℕ; zero; suc; z≤n; s≤s)
open import Data.Nat.Properties using ()
open import Data.Fin using (Fin; zero; suc; _≤_)
open import Relation.Binary.PropositionalEquality

data Mono : ℕ → ℕ → Set where
  nil : ∀ {n} → Mono zero n
  new : ∀ {n m} → Mono n       m       → Mono (suc n) (suc m)

phadej

title	author
Glassery	Oleg Grenrus

After I have improved the raw performance of optika – a JavaScript optics library, it's time to make the library (feature-)complete and sound. Gathering and classifying all possible optic types, gives us a reference point

phadej

import Data.Coerce
import Data.Monoid

-- This combinator is based on ala' from Conor McBride's work on Epigram.
alaf :: (Coercible n o, Coercible n' o')
     => (o -> n) -> ((a -> n) -> b -> n') -> (a -> o) -> b -> o'
alaf _ = coerce

myfoldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
myfoldl f z xs = alaf (Dual . Endo) foldMap (flip f) xs z