Types van types: Haskell's Kind-systeem

We beginnen bij het begin: met Waarden.

Waarden

Dit zijn de constructen die we in onze programma's manipuleren, zoals 1, 2, True, "hello", etc. In de context van functioneel programmeren worden ze ook wel "terms" genoemd. Het zijn de zaken die we consumeren, creëren, berekenen en als output genereren. Het beheren en manipuleren van waarden vormt een groot deel van de praktijk van programmeren en software engineering.

We werken dagelijks met verschillende waarden. Net als wezens in een fantasy-setting behoren waarden die bepaalde kenmerken delen — en die op dezelfde manier worden gemaakt, gebruikt en gemanipuleerd — tot dezelfde soort. Formeel worden deze "soorten" Types genoemd.

Types

Types zijn groepen van gerelateerde waarden. Met andere woorden: het concept van een type biedt ons een manier om collectief te verwijzen naar een groep gerelateerde waarden. In veel programmeertalen gebruiken we woorden als Int, String, Bool, Text, etc. om een type aan te duiden.

Naar mijn mening is het belangrijkste voordeel van het groeperen van waarden in types de abstractie. Types informeren ons — zowel de programmeur als de compiler — over de kenmerken van een waarde en de soorten bewerkingen die er wel of niet op of mee kunnen worden uitgevoerd. Denk aan wapenklassen in een game. In veel RPG's bepalen de wapenklassen welke soorten aanvallen je kunt uitvoeren of welke vaardigheden je ermee kunt gebruiken; types doen hetzelfde voor waarden.

Als we dit een stap verder nemen, zou je jezelf kunnen afvragen: hoe classificeren we types? Hebben we dat überhaupt nodig? En waarom? Om die vragen te beantwoorden, moeten we het domein van Kinds betreden.

Kinds

Kinds staan tot types wat types staan tot waarden. Mijn intuïtie voor het Kind-systeem is dat het een manier van classificatie is voor alles op type-niveau. Je zou denken dat "alles op type-niveau" simpelweg verwijst naar alledaagse types, maar in Haskell (en een paar andere talen) bestaan er andere type-niveau constructen, zoals type-niveau getallen (van Kind Nat), type-niveau strings (van Kind Symbol), of de constraints van Typeclasses (van Kind Constraint).

We gaan hier niet diep op ingaan, maar Nats en Symbols verschijnen vaak in contexten van type-level programming. Aan de andere kant zijn entiteiten van Kind Constraint waarschijnlijk bekender, omdat ze voor het grootste deel gewoon (volledig toegepaste) Typeclasses zijn. Bijvoorbeeld: de Show Typeclass behoort tot de Kind Type -> Constraint, en Show Int behoort tot de Kind Constraint.

Reguliere types behoren tot de Kind Type. Verwarrend, ik weet het. Type-constructoren — zaken als Maybe, Either, Last, Proxy, Dual, etc. — hebben een Kind die wordt bepaald door zowel hun ariteit als de Kind van hun parameters, zoals getoond in de onderstaande tabel.

Waarde	Type-niveau construct	Kind
1	Int	Type
True	Bool	Type
not	Bool -> Bool	Type
[1, 2, 3]	[Int]	Type
Just "hello"	Maybe String	Type
Right 5	Either String Int	Type
Maybe	Type -> Type	Type -> Type
[] (de lijst type-constructor)	Type -> Type	Type -> Type
Either	Type -> Type -> Type	Type -> Type -> Type
Either String	Type -> Type	Type -> Type
Three (van data Three a b c = …)	Type -> Type -> Type -> Type	Type -> Type -> Type -> Type
5 (een type-niveau getal)	Nat (GHCi print Natural)	Nat
"hello" (een type-niveau string)	Symbol	Symbol
Show Int	Constraint	Constraint
Show	Type -> Constraint	Type -> Constraint
Functor	(Type -> Type) -> Constraint	(Type -> Type) -> Constraint
Compose (vereenvoudigd)	(Type -> Type) -> (Type -> Type) -> Type -> Type	(Type -> Type) -> (Type -> Type) -> Type -> Type

* vs Type

In oudere documentatie en in sommige GHC-foutmeldingen zul je zien waar ik Type schrijf. Dit is hetzelfde. Voor zover ik weet is een synoniem voor Type en vice versa. * is de oudere naam, en GHC is van plan deze te deprecaten (-Wall waarschuwt al wanneer je het gebruikt).

Leuk feit: Technisch gezien zijn reguliere types ook type-constructoren; type-constructoren zonder parameters. Je zult ze aangeduid zien worden als "nullary type constructors".

Zonder Kinds zou er naar mijn mening geen manier zijn om type-niveau constructen zoals Maybe, Maybe Int en Show van elkaar te onderscheiden. Afhankelijk van waar je staat in je Haskell-reis is het voordeel van deze andere type-niveau entiteiten misschien niet direct duidelijk, maar ik kan je verzekeren dat ze er allemaal voor zorgen dat het Haskell-typesysteem expressiever wordt. Hierdoor kunnen we meer zaken in het typesysteem vastleggen, wat het makkelijker maakt om veiligere programma's te schrijven.

Higher-Kinded Types (HKTs)

We hebben eerder genoemd dat types ons in staat stellen om te abstraheren over waarden. Dit betekent dat we collectief naar een set waarden kunnen verwijzen via hun type. Op dezelfde manier benoemen we met een bepaalde Kind een collectie van type-niveau constructen. Bijvoorbeeld: de Kind Type -> Type verwijst collectief naar alle type-constructoren die één regulier type als argument nemen; dat omvat zaken als Maybe, maar ook partiële applicaties zoals Either String of Three Int String. Evenzo verwijst de Kind Type -> Type -> Type collectief naar alle type-constructoren die twee reguliere types als argumenten nemen. Om dit terug te brengen naar het waarde/term-niveau: dit is vergelijkbaar met functiesignaturen. Een functiesignatuur van Int -> Bool verwijst collectief naar alle functies die een Int als argument nemen en een Bool teruggeven.

We weten nu dat een signatuur zoals Int -> Bool verwijst naar een set functies, maar hoe zit het met iets als (Int -> Int) -> Bool? Wat betekent dat? Die signatuur representeert alle functies die een boolean teruggeven, maar pas nadat ze een functie met een signatuur van Int -> Int als argument hebben geaccepteerd. Dit type signatuur komt veel voor, en functies met dit soort signaturen worden higher-order functions genoemd.

Wat gebeurt er als we dit idee extrapoleren naar het Kind-niveau? Wat als we de Type parameter in Type -> Type vervangen door (Type -> Type)? Nou, voor het begin krijgen we een signatuur zoals (Type -> Type) -> Type. We weten dat Type de Kind is voor alle reguliere types en Type -> Type de Kind is voor alle type-constructoren die een enkel regulier type als argument nemen. Als we dat combineren, betekent het dat de signatuur (Type -> Type) -> Type de Kind representeert voor alle type-niveau constructen die een type-constructor als argument nemen.

Zie je waar ik heen ga? Net zoals functies met signaturen zoals (Int -> Int) -> Bool higher-order functions worden genoemd, worden type-constructoren met Kinds zoals (Type -> Type) -> Type of (Type -> Type) -> (Type -> Type) -> Type collectief higher-Kinded types of kortweg HKT's genoemd.

Hier is een klein voorbeeld:

data Wrap (f :: Type -> Type) = Wrap (f Int)

Wrap neemt een type-constructor f en plaatst daar een Int in, dus de Kind is (Type -> Type) -> Type. Wrap Maybe is een regulier type, en dat is Wrap [] ook. Wrap (Just 5) en Wrap [1, 2, 3] zijn waarden van respectievelijk deze types. Compose uit de eerdere tabel is een ander voorbeeld, maar dan met meer parameters.

Vanuit een andere hoek bekeken: als geparametriseerde types zoals Maybe of Either zijn wat andere talen "generics" noemen, dan zijn HKT's generics die andere generics als argumenten kunnen nemen.

Het concept van HKT's, in combinatie met Typeclasses, geeft ons de mogelijkheid om bepaalde functionaliteit te implementeren op type-niveau constructen. Dat is nuttig omdat het ons in staat stelt om operaties in veel meer contexten te hergebruiken. Ter illustratie nemen we Functor :: (Type -> Type) -> Constraint. Functor is zelf geen HKT, aangezien de Kind eindigt op Constraint en niet op Type. Echter, de parameter is een type-constructor, wat het higher-Kinded maakt.

Als een type-constructor een Functor-instantie heeft, kunnen we met de fmap-functie over de inhoud mappen. Bovendien, dankzij de higher-Kinded aard van Functor, hoeven we slechts één Functor-instantie te definiëren voor een passend Kind-type-constructor (specifiek Type -> Type) om fmap te kunnen gebruiken met elke specialisatie van die type-constructor. Wat ik bedoel is: omdat we de Functor-instantie definiëren op bijvoorbeeld Maybe en niet op een Maybe a, kunnen we fmap gebruiken op alle concrete versies van Maybe a (Maybe Int, Maybe String, Maybe Bool, etc.). Sterker nog, het kan niet anders: de Kind-signatuur van Functor accepteert alleen type-constructoren van Kind Type -> Type, dus iets als Maybe Int (van Kind Type) is geen kandidaat. De instantie hoort bij Maybe zelf. Dit principe geldt voor alle andere higher-Kinded Typeclasses en passend Kind-type-constructoren.

In niet-technische termen: neem een kom om uit te eten. Maak de kom zelf magnetronbestendig, en je kunt hem gebruiken om elk voedsel dat je erin doet op te warmen. In dit geval is de kom onze "passend Kind-type-constructor"; de standaard die bepaalt of iets "magnetronbestendig" is, is onze higher-Kinded Typeclass (zoals Functor); het "magnetronbestendig" label dat we op onze kom plakken is de Typeclass-instantie; en de kom met eten die we in de magnetron kunnen zetten, representeert een specialisatie van onze type-constructor. Ook hier kan het niet anders: niemand certificeert een kom soep als magnetronbestendig. Het label hoort bij de kom en is geldig ongeacht de inhoud van de kom.

Higher-Kinded Data (HKD)

Higher-Kinded data, of kortweg HKD, is de naam van een patroon waarbij een datatype, in plaats van een type-niveau ding, één of meer type-constructoren als parameters neemt en deze gebruikt om sommige of alle van zijn velden te wrappen. Men zou dit "geavanceerd" kunnen noemen, maar het is eigenlijk vrij eenvoudig zodra je higher-Kinded types begrijpt. Hier is een voorbeeld:

-- De `f` parameter is een type-constructor, wat `Profile` higher-Kinded maakt
data Profile (f :: Type -> Type) = Profile
{ age :: f Int
, name :: f String
, profession :: f String
, address :: f String
}

-- `f = Identity`: elk veld moet aanwezig zijn
grace :: Profile Identity
grace = Profile (Identity 37) (Identity "Grace") (Identity "Computer scientist") (Identity "New York")

-- `f = Maybe`: elk veld kan ontbreken, zoals bij een half ingevuld aanmeldingsformulier
draft :: Profile Maybe
draft = Profile Nothing (Just "Grace") Nothing Nothing

-- `f = Const String`: elk veld bevat een `String`, ongeacht het type, zoals een formulierlabel
labels :: Profile (Const String)
labels = Profile (Const "Age") (Const "Name") (Const "Profession") (Const "Address")

Laten we hier dieper op ingaan met een voorbeeld uit mijn redis-haskell project, waar ik ondersteuning toevoegde voor getypeerde Redis-configuraties afkomstig van zowel command-line opties als opties gedefinieerd in een redis.conf bestand.

Om dit te implementeren, had ik een datatype-representatie nodig van een Redis-configuratie met de velden die ik wilde ondersteunen. Het probleem waar ik tegenaan liep was duplicatie. Mijn eerste idee was een gewoon record-type, maar het moest twee verschillende contexten ondersteunen:

1. Een standaardconfiguratie waarbij alle velden beschikbaar zijn, geïnitialiseerd met hun officiële standaardwaarden.
2. Command-line configuraties en redis.conf configuraties waarbij velden nullable moeten zijn.

Mijn eerste richtingskeuze was om twee record-types te definiëren: één waar de veldtypes "kaal" waren, en een ander waar ze gewrapt waren in Last.

data RedisConfig = RedisConfig
{ rdbFileDirPath :: SomeBase Dir
, rdbFilenamePath :: Path Rel File
, useRDBCompression :: Bool
, genRdbChecksum :: Bool
, port :: Int
}
deriving stock (Generic)

data PartialRedisConfig = PartialRedisConfig
{ rdbFileDirPath :: Last (SomeBase Dir)
, rdbFilenamePath :: Last (Path Rel File)
, useRDBCompression :: Last Bool
, genRdbChecksum :: Last Bool
, port :: Last Int
}
deriving stock (Generic)

Waarom Last? De <> operator van Maybe vertrouwt op de Semigroup-semantiek van het type dat het bevat, tenzij een van de operanden Nothing is. Bovendien zouden voor deze werking al onze gewrapte veldtypes een Semigroup-instantie moeten hebben. Bool en Int hebben die niet. En zelfs voor types die dat wel hebben, zou <> de twee waarden combineren in plaats van er één te kiezen. Last behoudt de laatst aanwezige waarde, waardoor latere bronnen eerdere waarden kunnen overschrijven.

Ik was geen fan van deze aanpak omdat ik één "single source of truth" wilde voor de ondersteunde configuratieveldnamen en types. Met twee datatypes zou het makkelijk zijn om één variant aan te passen en te vergeten de andere bij te werken.

Een optie zou zijn om slechts één Redis-configuratietype te hebben waarbij elk veld in Last is gewrapt. Aangezien Last de meest rechtse Just-waarde behoudt, zou defaults <> confFileOpts <> cliOpts de command-line opties prioriteit geven, gevolgd door de redis.conf opties en dan de standaardwaarden. Precies de semantiek die we willen. Het probleem was echter het uiteindelijke resultaat. Het zou nog steeds een record zijn met alle velden gewrapt in Last, ook al zou de combinatie met het standaardrecord (defaults) garanderen dat alle velden een waarde hadden. Bijgevolg zou elke plek die uit die uiteindelijke configuratie leest, een Last-waarde moeten unwrappen die nooit Nothing kon zijn.

Dus, opnieuw: ik had twee variaties van mijn configuratietype nodig: een partiële voor het samenvoegen, en een volledige voor de standaardwaarden en het gebruik door de rest van de server. Wat ik niet wilde, was twee definities.

Om dit te bereiken, kwam ik uit op een definitie zoals deze:

data RedisConfigF (f :: Type -> Type) = RedisConfigF
{ rdbFileDirPath :: f (SomeBase Dir)
, rdbFilenamePath :: f (Path Rel File)
, useRDBCompression :: f Bool
, genRdbChecksum :: f Bool
, port :: f Int
}
deriving stock (Generic)

RedisConfigF is een higher-Kinded datatype. Het is higher-Kinded omdat de f parameter van Kind Type -> Type is. Dat maakt RedisConfigF zelf van Kind (Type -> Type) -> Type. Dit gaf me één datatypedefinitie voor beide contexten. Voor standaardwaarden en de uiteindelijke samengevoegde configuratie is f = Identity, en voor het geval waarin veldwaarden mogelijk niet aanwezig zijn, is f = Last.

Om te mergen maken we gebruik van de Semigroup-instantie voor Last om de configuratierecords van de redis.conf opties en de CLI-opties te combineren. Daarna vullen we de gaten op met de standaardwaarden.

Daarna krijgen we een record van type RedisConfigF Identity terug met alle velden ingevuld. Met f = Identity is elk veld echter nog steeds gewrapt in Identity, wat bij toegang moet worden unwrapped. De echte code automatiseert dit unwrappen.

In elk geval is dit de kracht en het nut van higher-Kinded datatypes. Een andere interessante use-case die ik heb gebruikt was RedisConfigF voor de associatie van veld-parsers. Met f = Const (Text, ReadM PartialRedisConfig) bevat hetzelfde record de redis.conf naam en de parser van elk veld, zodat de compiler me waarschuwt als ik een veld toevoeg maar vergeet er een naam en parser aan te koppelen.

Barbies Ik weet dat de barbies bibliotheek bestaat voor het werken met higher-Kinded data zoals dit, maar het voelde eenvoudiger en leerzamer om zelf de dingen te bouwen die ik voor deze specifieke use-case nodig had.

Aangepaste Kinds

Het laatste waar ik op wil ingaan zijn aangepaste Kinds. Net zoals je je eigen types kunt maken, kun je je eigen Kinds maken. Aangepaste Kinds zijn onze eigen type-niveau constructen, nuttig voor het promoten van informatie naar het typesysteem. Voorbeeld:

{-# LANGUAGE DataKinds #-}
data Person = Person Symbol Symbol Nat

Hier hebben we een data-declaratie die via de DataKinds extensie is gepromoveerd tot een Kind. In essentie breidt deze extensie de functionaliteit van de data-declaratie syntax uit, zodat data-declaraties zowel Kinds als datatypes definiëren. In het bovenstaande snippet:

• Person is de naam van ons aangepaste datatype én Kind.
• Person Symbol Symbol Nat is een beschrijving van de structuur/vorm van de type-niveau entiteiten die leden zijn van de Kind.
• 'Person :: Symbol -> Symbol -> Nat -> Person is de type-constructor voor het maken van type-niveau entiteiten van Kind Person.
• Person :: Symbol -> Symbol -> Nat -> Person is de data-constructor van het type Person.

Een lid van de Kind Person ziet er zo uit:

type Ada = 'Person "Ada" "Lovelace" 21   -- Ada :: Person

Ticks & Puns

Je hebt misschien de tick gezien in 'Person. Deze is bedoeld om een "pun" te disambigueren. In deze context is een pun wanneer een type en zijn constructor dezelfde naam delen, zoals data Person = Person …. Normaal gesproken is dit prima omdat Haskell types en terms in aparte namespaces houdt. Echter, zodra DataKinds is ingeschakeld en de data-constructor is gepromoveerd, kunnen beide namen (type en data-constructor) op type-niveau worden gebruikt. Hoe verwijzen we dan naar de gepromoveerde constructor als gewone Person al het type en de Kind betekent? De tick stelt ons in staat om expliciet naar de constructor te verwijzen: 'Person.

Wanneer de namen niet botsen (zoals data Person = MkPerson …), is de tick optioneel. Sinds GHC 9.4 adviseert GHC om deze standaard niet meer te schrijven. In ons Person-voorbeeld botsen de namen echter wel, dus is de tick vereist.

Let op dat Person zowel als type als Kind voorkomt. Sinds GHC 8 wordt elke Kind namelijk ook beschouwd als een type. Het is een beetje zoals je tegelijkertijd ouder en kind kunt zijn: een ouder voor je kinderen, en een kind voor je eigen ouders. Person werkt hetzelfde: het is de Kind waartoe Ada behoort, en het is ook een type dat behoort tot de Kind Type.

Daarnaast kunnen sommige Kinds "uninhabited" (onbewoond) zijn, net zoals sommige types dat zijn. Bijvoorbeeld: Int is als type bewoond door waarden, maar als Kind onbewoond door type-niveau constructen. Omgekeerd is Symbol onbewoond als type, maar bewoond door type-niveau string literals als Kind. Het is precies om deze reden dat ons Person type geen waarden kan hebben op term-niveau, maar wel bewoond kan zijn op Kind-niveau.

Bool is interessant omdat het zowel als type als Kind bewoond is. Dat geldt ook voor Nat (een alias voor Natural).

Type	Leden als type (waarden)	Leden als Kind (types)
Int	0, -3, …	geen
Symbol	geen	"Ada", "port", …
Bool	True, False	'True, 'False
Nat	0, 21, …	0, 21, … (type-level literals)

Laten we dit terugbrengen naar de redis-haskell use-case. In mijn PR had ik twee stukken data nodig voor elk veld in mijn RedisConfigF type: de redis.conf key die bij een veldnaam hoort en het type. In eerste instantie definieerde ik aparte type-synoniemen:

type RDBFileDir = SomeBase Dir
type RDBFileDirConfigFieldName = "dir"
type RDBFilename = Path Rel File
type RDBFilenameConfigFieldName = "dbfilename"
-- …één paar per veld

Ik probeerde ook type-niveau tuples voor betere inkapseling:

type RDBFileDir  = '("dir", SomeBase Dir)          -- Kind: (Symbol, Type)
type RDBFilename = '("dbfilename", Path Rel File)

Tuple pun: De tick werkt hier op dezelfde manier. Tuple-syntax is ook een pun, aangezien (a, b) zowel het tuple-type als de constructor benoemt.

Maar dat zou hetzelfde zijn als het gebruik van een anoniem product-type op term/waarde-niveau. Iets als (Symbol, Type) is structureel. Elke twee zulke paren zouden dezelfde Kind zijn, ongeacht de bedoeling. Daarom besloot ik mijn eigen aangepaste Kind te maken, ConfigField, dat nominaal, semantisch, zelfdocumenterend is en onmogelijk te verwarren is met een andere (Symbol, Type) pair.

Hier is de definitie, waarbij de velden uit de eerdere snippets zijn herschreven om het te gebruiken:

data ConfigField = ConfigField Symbol Type  -- met DataKinds is dit ook een Kind
type RDBFileDir        = 'ConfigField "dir"            (SomeBase Dir)
type RDBFilename       = 'ConfigField "dbfilename"     (Path Rel File)
type UseRDBCompression = 'ConfigField "rdbcompression" Bool
type GenRDBChecksum    = 'ConfigField "rdbchecksum"    Bool
type RedisPort         = 'ConfigField "port"           Int

Nu leven de redis.conf key en het Haskell-type van elk veld samen in één ConfigField. Met behulp van andere type-niveau mechanismen kunnen we die informatie op term-niveau raadplegen, waardoor duplicatie niet nodig is. We doen dit op een paar plekken met getConfigFieldName: in de command-line parser, waar elke key tevens als flag-naam dient ("dir" wordt --dir), en in de redis.conf parser.

Conclusie

Ter samenvatting: waarden zijn gegroepeerd in types, en types zijn gegroepeerd in Kinds. Elk patroon in dit artikel bouwt daarop voort. Higher-Kinded types stellen ons in staat types te definiëren die andere type-constructoren als argumenten nemen, zoals Wrap of Compose. Het Higher-Kinded data patroon gaf me één configuratie-record type dat zowel partieel als compleet kon zijn. En een aangepaste Kind stelde me in staat om de redis.conf key van elk configuratieveld bij het type te houden, zodat deze twee niet uit elkaar konden groeien.