Soham Chowdhury mrkgnao

Notes on adding Constraint Kinds to Rust

Background: Constraint Kinds

a trait can be thought of as a type operator generating a "constraint" - what in Rust would usually be called a bound. For example:

// Declares a new item `Foo` with kind `type -> constraint`
trait Foo { }

	# download corpus from https://www.ngrams.info

	corpus = open('5-grams non case sensitive.txt')
	corpus = [' '.join(line.split()[1:]) for line in corpus]

	love = 'i love you'

	lines = [line for line in corpus if line.find(love) >= 0]
	lines = [line.rjust(len(line) - line.find(love) + max([line.find(love) for line in lines])) for line in lines]
	lines = [line.replace(love, ' ' * len(love)) for line in lines]


	{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
	TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
	TypeOperators, TypeApplications, AllowAmbiguousTypes,
	TypeInType, StandaloneDeriving #-}

	import Data.Singletons.TH -- singletons 2.4.1
	import Data.Kind

	-- some standard stuff for later examples' sake

	-- Note: There is a more complete explanation at https://github.com/hwayne/lets-prove-leftpad/tree/master/idris
	import Data.Vect

	-- `minus` is saturating subtraction, so this works like we want it to
	eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
	eq_max n Z = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl
	eq_max Z (S _) = Refl
	eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl

	-- The type here says "the result is" padded to (maximum k n), and is padding plus the original

	theory Leftpad
	imports Main
	begin

	definition leftPad :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list"
	where "leftPad padChar targetLength s ≡ replicate (targetLength - length s) padChar @ s"

	definition isPadded :: "'a ⇒ 'a list ⇒ 'a list ⇒ bool"
	where "isPadded padChar unpadded padded ≡ ∃ n. set (take n padded) ⊆ { padChar } ∧ drop n padded = unpadded"

	{-# LANGUAGE DeriveGeneric #-}
	{-# LANGUAGE DerivingStrategies #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE GeneralizedNewtypeDeriving #-}
	{-# LANGUAGE TemplateHaskell #-}
	{-# LANGUAGE TypeApplications #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE UndecidableInstances #-}

	module Via where

	-- Response to
	-- https://gist.github.com/sjoerdvisscher/e8ed8ca8f3b6420b4aebe020b9e8e235
	-- https://twitter.com/sjoerd_visscher/status/975375241932427265

	{-# Language QuantifiedConstraints, TypeOperators, RankNTypes, GADTs, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, InstanceSigs #-}

	import Data.Coerce

	type f ~> g = forall x. f x -> g x

	{-# language TypeInType, QuantifiedConstraints, ConstraintKinds, RankNTypes, UndecidableInstances, MultiParamTypeClasses, TypeFamilies, KindSignatures #-}

	module QC where

	import Data.Constraint
	import Data.Functor.Contravariant
	import Data.Kind
	import Data.Profunctor

	type C = (Type -> Type) -> (Type -> Type -> Type) -> Constraint

	let List/replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate in

	let File = Natural in
	let Rank = Natural in
	let Square = { file : File, rank : Rank } in
	let Move = { from : Square, to : Square } in

	let Side = < white : {} \| black : {} > in
	let white = < white = {=} \| black : {} > in
	let black = < black = {=} \| white : {} > in

	{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances #-}
	{-# LANGUAGE LambdaCase, FlexibleContexts, UndecidableInstances, TypeOperators, DataKinds, MultiParamTypeClasses #-}
	module Sem where

	import Data.Algebra
	import Data.Constraint
	import Data.Constraint.Class1
	import Data.Functor.Free

	class BaseSem a where