| title | Glassery |
|---|---|
| author | 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
| cabal-version: 3.0 | |
| name: callback-exception | |
| version: 0 | |
| executable problem | |
| build-depends: base | |
| include-dirs: include | |
| hs-source-dirs: src | |
| main-is: problem.hs |
| {-# 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 |
| module SystemF where | |
| open import Agda.Primitive | |
| open import Prelude | |
| open import Data.List | |
| weaken-∈ : ∀ {a : Set} (Γ₁ : List a) {Γ x y} → x ∈ (Γ₁ ++ Γ) → x ∈ (Γ₁ ++ y ∷ Γ) | |
| weaken-∈ [] (zero refl) = suc (zero refl) | |
| weaken-∈ [] (suc i) = suc (suc i) | |
| weaken-∈ (x ∷ Γ₁) (zero p) = zero p |
| {-# LANGUAGE RankNTypes, ScopedTypeVariables #-} | |
| {-# OPTIONS_GHC -Wall #-} | |
| module Parts where | |
| import Data.Kind | |
| import Control.Applicative (liftA2) | |
| import Data.Function | |
| -- in blogs |
| 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. |
| {-# LANGUAGE ConstraintKinds #-} | |
| {-# LANGUAGE DeriveGeneric #-} | |
| {-# LANGUAGE FlexibleContexts #-} | |
| {-# LANGUAGE FlexibleInstances #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE KindSignatures #-} | |
| {-# LANGUAGE MultiParamTypeClasses #-} | |
| {-# LANGUAGE RankNTypes #-} | |
| {-# LANGUAGE TypeApplications #-} | |
| {-# LANGUAGE TypeOperators #-} |
| {-# 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 () |
| -- 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 ℕ |
