Mikolaj Konarski Mikolaj

GADTs That Can Be Newtypes and How to Roll 'Em

I think many people know about Data.Some.Newtype⁠—⁠it uses quite a cute (and cursed) trick to encode a simple existential wrapper as a newtype, hence avoiding an unwanted indirection in the runtime representation.

But there's more to data than existentials⁠—⁠so how far do these tricks go? The answer is: surprisingly far! Let's see what other GADTs we can slim down.

Preliminaries

Company:

HOC: Towards an Optimal Computer: why interaction paradigm can improve computers.
HOC: Can we build an optimal processor?: like above, but as a tweet.
HOC: Complete Historical Overview: the lore behind HOC's creation.

Theory:

Interaction Combinators - Y.Lafont 1997: a concurrent model of computation
Symmetric Interaction Combinators - Damiano Mazza 2009: a symmetric variant (used by HVM)
The Optimal Implementation of Functional Programming Languages - best book to learn
[BOHM](https://www.cambridge.org/core/services/aop-cambridge-core/content/

notacji C7+ używam jako skrótu Cmaj7 
  (a więc nie oznacza to C z podniesioną kwintą i septymą małą (C5+7), tylko C z septymą wielką) 
d7(f-c-d) oznacza, że tak można grać prawą rękę akordu d7
(D) oznacza, że można tu zagrać D lub nie zagrać
d0 to czterodźwięk D zmniejszony (D-F-Ab-Cb)
d07 to czterodźwięk D półzmniejszony (D-F-Ab-C)
E< to trójdźwięk E zwiększony
|| oznacza początek nowego taktu

dziękuję wszystkim oryginalnym autorom, krytykom, muzom

	{-# LANGUAGE BlockArguments #-}

	module InlineFix (
	Rec,
	inlineFix,
	Church, (\|&), _0, _1, _2, _3, _4, _5, _6, _7, _8, _9,
	) where

	import GHC.Exts (inline)
	import Data.Function (fix)

	{-# LANGUAGE TemplateHaskellQuotes #-}
	{-# LANGUAGE GADTs #-}
	module Pat3 where

	import qualified Language.Haskell.TH as TH (Code, Q,)
	import qualified Language.Haskell.TH.Syntax as TH (Lift(..))
	import Data.Functor.Identity

	type Code = TH.Code TH.Q

	{-# LANGUAGE QuantifiedConstraints, BlockArguments, LambdaCase #-}

	module Rec where

	import Data.Functor.Product (Product(..))
	import Data.Functor.Sum (Sum(..))
	import Data.Kind (Type, Constraint)
	import Control.Arrow ((&&&), (\|\|\|))

	cabal-version: 2.4
	name: Squeeze
	version: 0.1.0.0
	author: Ignat Insarov
	maintainer: [email protected]

	library
	hs-source-dirs: .
	build-depends: base, distributive
	default-language: Haskell2010

	import qualified Data.Set as S
	import Data.Set (Set)
	import Data.Char (isLower)
	import Data.Ord (comparing, Down (Down))
	import Data.List (sortBy, subsequences, minimumBy, maximumBy)
	import Control.Monad.Trans.Writer.CPS
	import Data.Monoid
	import Data.Foldable (traverse_)

	wordFilter :: String -> Bool

	// Copyright (c) 2021 Francesco Mazzoli <[email protected]>
	//
	// Permission to use, copy, modify, and distribute this software for any
	// purpose with or without fee is hereby granted, provided that the above
	// copyright notice and this permission notice appear in all copies.
	//
	// THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
	// WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
	// MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
	// ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES

	{-# OPTIONS --cubical --type-in-type #-}
	module Mokhov where

	open import Cubical.Foundations.Everything
	open import Cubical.Data.Sum
	open import Cubical.Data.Prod
	open import Cubical.Data.Unit

	record Mokhov (F : Set → Set) (G : Set → Set) (A : Set) : Set where
	constructor mokhov