Skip to content
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

unify Combine and CombineTypes #2651

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

unify Combine and CombineTypes #2651

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 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
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
49 changes: 40 additions & 9 deletions dhall/src/Dhall/TypeCheck.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -801,15 +801,24 @@
Combine _ mk l r -> do
_L' <- loop ctx l

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

let l'' = quote names l'

_R' <- loop ctx r

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

xLs' <- case _L' of
VRecord xLs' ->
return xLs'
let r'' = quote names r'

-- The `Combine` operator should now work on record terms and also on record types.
-- If both sides are record terms, we set leftTypeOrRecord and rightTypeOrRecord to (Left record_fields).
-- If both sides are record types, we set both of them to (Right (Type, record_fields)).
-- Then we match the pair (leftTypeOrRecord, rightTypeOrRecord) to make sure we catch errors.
leftTypeOrRecord <- case (_L', l') of
(VRecord xLs', _) -> return (Left xLs')

(VConst cL, VRecord xLs') -> return (Right (cL, xLs'))

_ -> do
let _L'' = quote names _L'
Expand All @@ -818,9 +827,12 @@
Nothing -> die (MustCombineARecord '∧' l'' _L'')
Just t -> die (InvalidDuplicateField t l _L'')

xRs' <- case _R' of
VRecord xRs' ->
return xRs'
-- Make sure both are on the Left (both record values) or on the Right (both record types).
rightTypeOrRecord <- case (leftTypeOrRecord, _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.

I think it would be better to first construct leftTypeOrRecord, then rightTypeOfRecord, and do the check that they are both Left or both Right afterwards in a separate step.

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 it would be better to first construct leftTypeOrRecord, then rightTypeOfRecord, and do the check that they are both Left or both Right afterwards in a separate step.

I'm not sure I understand your comment. It appears to me that my code already does what you say: it first constructs leftTypeOrRecord, then rightTypeOfRecord, and then checks that they are both Left or both Right in a separate expression.

Copy link
Collaborator

@mmhat mmhat Mar 18, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

What I mean is that you match on leftTypeOrRecord when you construct rightTypeOrRecord.
I think something like the following results in better error messages:

let isTypeOrRecord t = do
        _T <- loop ctx t

        let t' = eval values t
            
        case (_T, t') of
                (VRecord xs, _) -> return (Left xs)

                (VConst _T', VRecord xs) -> return (Right (_T', xs))

                _ -> do
                    let _T'' = quote names _T'

                    case mk of
                        Nothing -> die (MustCombineARecord '∧' l'' _T'')
                        Just k  -> die (InvalidDuplicateField k t _T'')

leftTypeOrRecord <- isTypeOrRecord l
rightTypeOrRecord <- isTypeOrRecord r

case (leftTypeOrRecord, rightTypeOrRecord)
    (Left ..., Left ...) -> ...
    (Right ..., Right ...) -> ...
    (Left ..., Right ...) -> die (TriedToCombineLitWithType ...)
    (Right ..., Left ...) -> die (TriedToCombineTypeWithLit ...)

(Left _, VRecord xRs', _) ->
return (Left xRs')

(Right _, VConst cR, VRecord xRs') -> return (Right (cR, xRs'))

_ -> do
let _R'' = quote names _R'
Expand All @@ -845,7 +857,26 @@

return (VRecord xTs)

combineTypes [] xLs' xRs'
let combineTypesCheck xs xLs₀' xRs₀' = 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)

case (leftTypeOrRecord, rightTypeOrRecord) of

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.ghc-9.8.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.ghc-9.8.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.ghc-9.4.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.ghc-9.4.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.ghc-9.2.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.ghc-9.2.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.ghc-8.10.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.ghc-8.10.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / ubuntu-latest - stack.ghc-8.10.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / macOS-latest - stack.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / macOS-latest - stack.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / windows-latest - stack.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / macos-13 - stack.yaml 

Pattern match(es) are non-exhaustive

Check warning on line 872 in dhall/src/Dhall/TypeCheck.hs

View workflow job for this annotation

GitHub Actions / macos-13 - stack.yaml 

Pattern match(es) are non-exhaustive
(Left xLs', Left xRs') -> do
combineTypes [] xLs' xRs'
(Right (cL, xLs'), Right (cR, xRs')) -> do
let c = max cL cR
combineTypesCheck [] xLs' xRs'
return (VConst c)


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