Last active
August 5, 2025 16:46
-
-
Save rybla/6c7bc3dbe3a4adbcff5718a090321203 to your computer and use it in GitHub Desktop.
dependent record fields in Haskell
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {- | |
| This module demonstrates a neat feature in Haskell that I commonly use in TypeScript. | |
| For example, in TypeScript, I often do something like this: | |
| ``` | |
| type Person | |
| = { name: string } | |
| & ( { isAnnotated: false } | |
| | { isAnnotated: true; annotation: string } ) | |
| ``` | |
| This is a simple example just to demonstrate the idea. | |
| Then I can do a sort of dependent pattern match like so: | |
| ``` | |
| function ex1(person: Person) { | |
| console.log(`name: ${person.name}`) | |
| if (person.isAnnotated) { | |
| console.log(`annotation: ${person.annotation}`) | |
| } | |
| } | |
| ``` | |
| And the type system will enforce that I only know that | |
| `person.annotation: string` if I have in context some check that | |
| `person.isAnnotated === true`. | |
| So how would you accomplish something like this in Haskell? | |
| With singletons of course! | |
| For an explanation of singletons in general: https://richarde.dev/papers/2012/singletons/paper.pdf | |
| -} | |
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE FlexibleContexts #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE OverloadedRecordDot #-} | |
| {-# LANGUAGE RankNTypes #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE StandaloneKindSignatures #-} | |
| {-# LANGUAGE TemplateHaskell #-} | |
| {-# LANGUAGE TypeApplications #-} | |
| {-# LANGUAGE TypeFamilies #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| {-# OPTIONS_GHC -Wno-missing-export-lists #-} | |
| {-# OPTIONS_GHC -Wno-missing-signatures #-} | |
| {-# OPTIONS_GHC -Wno-orphans #-} | |
| {-# OPTIONS_GHC -Wno-unused-do-bind #-} | |
| {-# OPTIONS_GHC -Wno-unused-top-binds #-} | |
| module DependentRecord where | |
| import Data.Singletons.TH (genSingletons) | |
| import GHC.Records (HasField (..)) | |
| $(genSingletons [''Bool]) | |
| -- A person that could have an annotation. Whether or not the person has an | |
| -- annotation is reflected in the phantom type parameter `isAnnotated`. The | |
| -- field `isAnnotated` isomorphic to a `Bool` that reflects the `isAnnotated` | |
| -- type. | |
| data Person isAnnotated = Person | |
| { name :: String, | |
| isAnnotated :: SBool isAnnotated, | |
| -- An unguarded field that could contain trivial data | |
| _annotation :: Annotation isAnnotated | |
| } | |
| -- The type of annotations is `String` if `isAnnotated ~ True` and trivial | |
| -- otherwise | |
| type family Annotation (isAnnotated :: Bool) where | |
| Annotation True = String | |
| Annotation False = () | |
| -- Guard the presence of an "annotation" field by a check that `isAnnotation` | |
| -- unifies with `True` | |
| instance (isAnnotated ~ True) => HasField "annotation" (Person isAnnotated) String where | |
| getField = getField @"_annotation" -- wraps the "_annotation" field | |
| ex1 :: Person isAnnotated -> IO () | |
| ex1 person = do | |
| -- Access a common field that exists no matter what `isAnnotated` is | |
| putStrLn ("name: " ++ person.name) | |
| -- Since `person.isAnnotated :: SBool isAnnotated`, which is a singleton, we | |
| -- can do dependent pattern matching on it i.e. since `person.isAnnotated` | |
| -- reflects the `isAnnotated` type, each branch of this pattern match will get | |
| -- the additional type information revealed by the value of | |
| -- `person.isAnnotated`. | |
| -- | |
| _ :: () <- case person.isAnnotated of | |
| STrue -> do | |
| -- Only in the case that `person.isAnnotated ~ True`, which is implied by | |
| -- `person.isAnnotated == STrue`, does the field "annotation" exist on | |
| -- `Person isAnnotated`. | |
| print ("annotation: " ++ person.annotation) | |
| SFalse -> do | |
| -- Using `person.annotation` here would yield a type error since `Person | |
| -- isAnnotation` only has an "annotation" field when `isAnnotation ~ True` | |
| return () | |
| print "end of ex1" | |
| -- Type inference also works! | |
| -- The typechecker infers: | |
| -- - `ex1 person` requires that `person : Person isAnnotated` for some `isAnnotated` | |
| -- - `person.annotation` requires that `HasField "annotation" (Person isAnnotated) _` | |
| -- - there is only one rule to derive `HasField "annotation" (Person isAnnotated) String`, | |
| -- and it requires `isAnnotated ~ True` | |
| -- Therefor, `person :: Person True` | |
| ex2 person = do | |
| ex1 person | |
| print ("name: " ++ person.name) | |
| print ("annotation: " ++ person.annotation) | |
| print "end of ex2" | |
| ex3 :: IO () | |
| ex3 = do | |
| ex2 | |
| ( Person | |
| { name = "Bob", | |
| isAnnotated = STrue, | |
| _annotation = "Bob is a great guy." | |
| } | |
| ) | |
| -- This causes a type error, since `ex2` requires it's input to be a `Person True` | |
| -- ex2 | |
| -- ( Person | |
| -- { name = "Bob", | |
| -- isAnnotated = SFalse, | |
| -- _annotation = () | |
| -- } | |
| -- ) | |
| print "end of ex3" |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment