gusbicalho

#lang pie

;; General

(claim Not
  (-> U U))
(define Not
  (λ (T)
    (-> T Absurd)))

gusbicalho

Metaphors

(Heads up: mostly just playing with ideas and types; no real use cases in sight. Also, I apologize upfront for the silly examples.)

You can use markdown-unlit to load this file as a Literate Haskell file. If you don't want to install it globally on your system, something like this should work:

gusbicalho

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}

module StagedPower where

import Language.Haskell.TH (Q, TExp)

type Code a = Q (TExp a)

gusbicalho

---------------------------- MODULE Convergence ----------------------------
EXTENDS TLC, Integers


abs(n) == IF n < 0 THEN -n ELSE n

(***************************************************************************
--algorithm Convergence

variables

gusbicalho

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE BangPatterns #-}

gusbicalho

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

gusbicalho

module StateMachine where

import Data.Foldable (foldlM)

data Init = Init
  deriving (Eq, Show)
data A = A Int
  deriving (Eq, Show)
data B = B String
  deriving (Eq, Show)

gusbicalho

(ns components-example
  (:require [com.stuartsierra.component :as component]))

(defprotocol Counter
  (get-c [this])
  (inc-c! [this]))

(defrecord SimpleCounter [counter]
  component/Lifecycle
  (start [this]

gusbicalho

Livros

• I Heart Logs
• Designing Data-Intensive Applications
• Building Microservices

Talks

• Construindo a NuConta
• Architecting a Modern Financial Institution

gusbicalho

{-# LANGUAGE
    DataKinds, DeriveGeneric, FlexibleContexts, FlexibleInstances, FunctionalDependencies,
    GADTs, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, TypeOperators,
    UndecidableInstances
#-}
module TypeLevelSets (
  ToSet, Add, Delete, Union, Difference
) where

  import GHC.TypeLits