effectfully

Basic QTT

Quantitative type theory (QTT) is an extension of dependent type theory which allows us to track the number of computational (non-erased) uses of variables in well-typed lambda terms. With such usage information, QTT allows us to combine dependent types with substructural types, such as linear, affine or relevant types.

While in a Martin-Löf style type theory typing judgments are of form x1 : A1, ..., xn : An ⊢ b : B, in QTT the bindings in the context

A Taxonomy of Self-Types

Part I: Introduction to Self-Types

Datatypes in the Formality programming language are built out of an unusual structure: the self-type. Roughly speaking, a self-type is a type that can depend or be a proposition on it's own value. For instance, the consider the 2 constructor datatype Bool:

Optics By Example Cheat Sheets

The following are appendices from Optics By Example, a comprehensive guide to optics from beginner to advanced! If you like the content below, there's plenty more where that came from; pick up the book!

Operators
Composition Guide
Substitution Guide
Optical Constarints and Types

Operator Cheat Sheet

Continued in Explicit Witnesses of Monoid Actions, Semigroup / Monoid / Applicative homomorphisms

Reddit discussion

My initial motivation for -XDerivingVia was deriving across isomorphisms.

Standard type-class encodings of isos turn out to be awkward due to overlap.

	{-# LANGUAGE DerivingStrategies #-}
	{-# LANGUAGE ImportQualifiedPost #-}
	{-# LANGUAGE PatternSynonyms #-}
	{-# LANGUAGE TemplateHaskell #-}
	{-# LANGUAGE ViewPatterns #-}

	module Bin (BinarySegment (..), bin) where

	import Control.Applicative ((<\|>))
	import Control.Monad (guard)

	{-# Language FlexibleInstances #-}
	{-# Language MultiParamTypeClasses #-}
	{-# Language FlexibleContexts #-}
	{-# Language UndecidableInstances #-}
	{-# Language DeriveTraversable #-}
	{-# Language NoStarIsType #-}
	{-# Language StandaloneKindSignatures #-}
	{-# Language RoleAnnotations #-}

	-- \| Dysfunctional dependencies

	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE OverloadedLabels #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE TypeApplications #-}

	module Main where

	import GHC.OverloadedLabels
	import GHC.Records

	{-# OPTIONS --without-K #-}

	{-
	Claim: finitary inductive types are constructible from Π,Σ,Uᵢ,_≡_ and ℕ, without
	quotients. Sketch in two parts.

	1. First, construction of finitary inductive types from Π, Σ, Uᵢ, _≡_ and binary trees.
	Here I only show this for really simple, single-sorted closed inductive types,
	but it should work for indexed inductive types as well.

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE UndecidableInstances #-}
	{-# LANGUAGE UnsaturatedTypeFamilies #-}

	import GHC.TypeLits
	import Prelude hiding (Functor, Semigroup)

	type Main = (Fizz <> Buzz) <$> (0 `To` 100)

	{-# LANGUAGE KindSignatures, DataKinds, FlexibleInstances, FlexibleContexts,
	FunctionalDependencies, TypeFamilies, TypeOperators,
	PatternSynonyms, UndecidableInstances, ConstraintKinds,
	TypeApplications, ScopedTypeVariables, CPP #-}

	module NamedDefaults (FillDefaults, fillDefaults, (!.)) where

	import Prelude (Maybe(..), id)
	import Data.Kind (Type)