Skip to content

unify Combine and CombineTypes #2651

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 30 commits into
base: main
Choose a base branch
from
Open

unify Combine and CombineTypes #2651

Show file tree
Hide file tree
Changes from 22 commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
b66de13
wip add the functionality of CombineTypes to Combine
winitzki Mar 13, 2025
e07a39e
wip
winitzki Mar 13, 2025
068d623
pretty-print //\\ as /\ now globlly
winitzki Mar 13, 2025
bb59a38
typechecking of record type /\ record type
winitzki Mar 13, 2025
f7c03e3
undo the formatting change because tests fail
winitzki Mar 14, 2025
d21abae
implement /\ reduction for record types
winitzki Mar 14, 2025
be4ea39
fix isNormalized
winitzki Mar 14, 2025
11a7b3c
add comment
winitzki Mar 17, 2025
8050d24
remove wrong import
winitzki Mar 17, 2025
8fe9623
refactor code for clarity
winitzki Mar 20, 2025
e7b55f0
Merge branch 'main' into feature/unify-Combine-and-CombineTypes
winitzki May 5, 2025
20dfebd
bump ci
winitzki May 7, 2025
5933b6a
bump ci
winitzki May 7, 2025
79d0da8
Merge branch 'main' into feature/unify-Combine-and-CombineTypes
winitzki May 14, 2025
189d572
bump ci
winitzki May 15, 2025
0bcc84d
bump ci
winitzki May 16, 2025
0ecadb1
bump ci
winitzki May 16, 2025
400549e
bump ci
winitzki May 17, 2025
43a8741
bump ci
winitzki May 17, 2025
5f51a3f
bump ci
winitzki May 18, 2025
7a5bca8
Merge branch 'main' into feature/unify-Combine-and-CombineTypes
winitzki Jun 18, 2025
7864ec9
bump ci
winitzki Jun 19, 2025
d7b782c
refactor to use combineTypesCheckingForFieldCollisions outside of loo…
winitzki Jun 19, 2025
53a5a3d
minor rewrite
winitzki Jun 19, 2025
df0330c
Add a better error message for the case of /\ on record terms or types
winitzki Jun 19, 2025
aa6fd30
implement better error messages
winitzki Jun 20, 2025
c942a3d
wip adding unit tests for CombineTypes feature
winitzki Jun 20, 2025
87845fa
add unit tests for new error messages
winitzki Jun 20, 2025
9557e57
better error messages and more unit tests
winitzki Jun 21, 2025
5cfc83c
Merge branch 'main' into feature/unify-Combine-and-CombineTypes
winitzki Jul 1, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions dhall/src/Dhall/Eval.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -318,6 +318,12 @@ vCombine mk t u =
t'
(VRecordLit m, VRecordLit m') ->
VRecordLit (Map.unionWith (vCombine Nothing) m m')
(VRecord m, u') | null m ->
u'
(t', VRecord m) | null m ->
t'
(VRecord m, VRecord m') ->
VRecord (Map.unionWith (vCombine Nothing) m m')
(t', u') ->
VCombine mk t' u'

Expand Down
16 changes: 12 additions & 4 deletions dhall/src/Dhall/Normalize.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -548,15 +548,20 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
kts' = traverse (traverse loop) kts
Combine cs mk x y -> decide <$> loop x <*> loop y
where
mergeFields (RecordField _ expr _ _) (RecordField _ expr' _ _) =
Syntax.makeRecordField $ decide expr expr'
decide (RecordLit m) r | Data.Foldable.null m =
r
decide l (RecordLit n) | Data.Foldable.null n =
l
decide (RecordLit m) (RecordLit n) =
RecordLit (Dhall.Map.unionWith f m n)
where
f (RecordField _ expr _ _) (RecordField _ expr' _ _) =
Syntax.makeRecordField $ decide expr expr'
RecordLit (Dhall.Map.unionWith mergeFields m n)
decide (Record m) r | Data.Foldable.null m =
r
decide l (Record n) | Data.Foldable.null n =
l
decide (Record m) (Record n) =
Record (Dhall.Map.unionWith mergeFields m n)
decide l r =
Combine cs mk l r
CombineTypes cs x y -> decide <$> loop x <*> loop y
Expand Down Expand Up @@ -949,6 +954,9 @@ isNormalized e0 = loop (Syntax.denote e0)
decide (RecordLit m) _ | Data.Foldable.null m = False
decide _ (RecordLit n) | Data.Foldable.null n = False
decide (RecordLit _) (RecordLit _) = False
decide (Record m) _ | Data.Foldable.null m = False
decide _ (Record n) | Data.Foldable.null n = False
decide (Record _) (Record _) = False
decide _ _ = True
CombineTypes _ x y -> loop x && loop y && decide x y
where
Expand Down
70 changes: 48 additions & 22 deletions dhall/src/Dhall/TypeCheck.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -801,34 +801,22 @@ infer typer = loop
Combine _ mk l r -> do
_L' <- loop ctx l

let l'' = quote names (eval values l)

_R' <- loop ctx r

let r'' = quote names (eval values r)
let _L'' = quote names _L'

xLs' <- case _L' of
VRecord xLs' ->
return xLs'
let l' = eval values l

_ -> do
let _L'' = quote names _L'
let l'' = quote names l'

case mk of
Nothing -> die (MustCombineARecord '∧' l'' _L'')
Just t -> die (InvalidDuplicateField t l _L'')
_R' <- loop ctx r

xRs' <- case _R' of
VRecord xRs' ->
return xRs'
let _R'' = quote names _R'

_ -> do
let _R'' = quote names _R'
let r' = eval values r

case mk of
Nothing -> die (MustCombineARecord '∧' r'' _R'')
Just t -> die (InvalidDuplicateField t r _R'')
let r'' = quote names r'

-- The `Combine` operator should now work on record terms and also on record types.
-- We will use combineTypes or combineTypesCheck below as needed for each case.
let combineTypes xs xLs₀' xRs₀' = do
let combine x (VRecord xLs₁') (VRecord xRs₁') =
combineTypes (x : xs) xLs₁' xRs₁'
Expand All @@ -845,7 +833,45 @@ infer typer = loop

return (VRecord xTs)

combineTypes [] xLs' xRs'
let combineTypesCheck xs xLs₀' xRs₀' = do
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we can pull this out of look and use it in both the Combine and CombineTypes cases?
Also, can we rename this to something more meaningful like checkForFieldCollisions?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Will do.

let combine x (VRecord xLs₁') (VRecord xRs₁') =
combineTypesCheck (x : xs) xLs₁' xRs₁'

combine x _ _ =
die (FieldTypeCollision (NonEmpty.reverse (x :| xs)))

let mL = Dhall.Map.toMap xLs₀'
let mR = Dhall.Map.toMap xRs₀'

Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR)

-- If both sides of `Combine` are record terms, we use combineTypes to figure out the resulting type.
-- If both sides are record types, we use combineTypesCheck and then return the upper bound of two types.
-- Otherwise there is a type error.
case (_L', l', _R', r') of
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Previously we threw a CombineTypesRequiresRecordType if we were combining types. Do you think its feasible to retain that behaviour, i.e. throw that error when we combine types and one of the other errors when we combine values?

Copy link
Collaborator Author

@winitzki winitzki Jun 19, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's think about what error behavior we need. The new operator /\ should report an error if it is applied to a record term and a non-record term; or to a record type and a non-record type; or to a term and a type.

  • { a = 0 } /\ 123 Error: Must combine records, instead got 123 .
  • { a : Bool } /\ Natural Error: CombineTypes requires a record type, instead got Natural.
  • { a : Bool } /\ { b = 0 }. What should be the error? CombineTypes requires a record type but instead got a record term { b = 0 }, or Must combine records but instead got a record type { a : Bool } ? I think we can just assume that the first operand is correct and the second one is wrong, and report CombineTypes requires a record type but instead got a record term { b = 0 }.

I will work on this tomorrow. It's definitely feasible to implement detailed error messages here.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For the last case, maybe something like:

The combine operator `/\` works either on two record literals or two record types. You provided expressions
  * `{a : Bool}`, which is a record type, and
  * `{b = 0}`, which is a record literal of type `{b : Natural }`.

Also, for the other cases we probably want a similar error message if both arguments are neither record term nor record type; For example if the expression was 1 /\ 2.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we need unit tests for all those cases. I don't see any unit tests.

Right now, an incorrect use of /\ gives an error CombineTypesRequiresRecordType that talks about //\\ instead. I'll work on fixing this now.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that would be great! Thank you for working on this!

Copy link
Collaborator Author

@winitzki winitzki Jun 20, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have changed the error messages, making them more detailed. I also added some unit tests to verify that those error messages are actually being generated. For instance, the tests verify that errors for the ∧ operator describe examples involving ∧, while errors for the ⩓ operator describe examples with ⩓.

(VRecord xLs', _, VRecord xRs', _) -> do
combineTypes [] xLs' xRs'

(VConst cL, VRecord xLs', VConst cR, VRecord xRs') -> do
let c = max cL cR
combineTypesCheck [] xLs' xRs'
return (VConst c)

(_, _, VRecord _, _) -> do
case mk of
Nothing -> die (MustCombineARecord '∧' l'' _L'')
Just t -> die (InvalidDuplicateField t l _L'')

(_, _, VConst _, _) -> do
case mk of
Nothing -> die (MustCombineARecord '∧' l'' _L'')
Just t -> die (InvalidDuplicateField t l _L'')

_ -> do
case mk of
Nothing -> die (MustCombineARecord '∧' r'' _R'')
Just t -> die (InvalidDuplicateField t r _R'')


CombineTypes _ l r -> do
_L' <- loop ctx l
Expand Down
Loading