From b66de13771b254f5be9739eeb35edf8cdf64c304 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 13 Mar 2025 15:26:08 +0100 Subject: [PATCH 01/10] wip add the functionality of CombineTypes to Combine --- dhall/src/Dhall/TypeCheck.hs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 9c2a30355..7cf42d6a1 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -801,11 +801,15 @@ infer typer = loop 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 + + let r'' = quote names r' xLs' <- case _L' of VRecord xLs' -> From e07a39ef60ce8f06bb72cc5a0d46ee395f26fdc2 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 13 Mar 2025 15:31:04 +0100 Subject: [PATCH 02/10] wip --- dhall/src/Dhall/TypeCheck.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 7cf42d6a1..6e7264a25 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -814,7 +814,7 @@ infer typer = loop xLs' <- case _L' of VRecord xLs' -> return xLs' - +-- or it can be VConst Type or similar, if we are doing /\ on two record types. _ -> do let _L'' = quote names _L' @@ -832,7 +832,7 @@ infer typer = loop case mk of Nothing -> die (MustCombineARecord '∧' r'' _R'') Just t -> die (InvalidDuplicateField t r _R'') - +-- TODO examine why this `combineTypes` is different from that defined in `CombineTypes _ l r`. let combineTypes xs xLs₀' xRs₀' = do let combine x (VRecord xLs₁') (VRecord xRs₁') = combineTypes (x : xs) xLs₁' xRs₁' From 068d6232893a61a5fc7f4e488d35484162ced479 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 13 Mar 2025 21:44:04 +0100 Subject: [PATCH 03/10] pretty-print //\\ as /\ now globlly --- dhall/src/Dhall/Pretty/Internal.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index fdd545d3c..4b9c7b305 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -432,8 +432,7 @@ combine ASCII = "/\\" combine Unicode = "∧" combineTypes :: CharacterSet -> Text -combineTypes ASCII = "//\\\\" -combineTypes Unicode = "⩓" +combineTypes = combine -- Replace //\\ by /\ as //\\ is now deprecated. prefer :: CharacterSet -> Text prefer ASCII = "//" From bb59a38385d7a5ef19eb28158dd4d5cc36dc5e6b Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 13 Mar 2025 22:27:33 +0100 Subject: [PATCH 04/10] typechecking of record type /\ record type --- dhall/src/Dhall/TypeCheck.hs | 41 ++++++++++++++++++++++++++++-------- 1 file changed, 32 insertions(+), 9 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 6e7264a25..8df8b9bf2 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -811,10 +811,11 @@ infer typer = loop let r'' = quote names r' - xLs' <- case _L' of - VRecord xLs' -> - return xLs' --- or it can be VConst Type or similar, if we are doing /\ on two record types. + leftTypeOrRecord <- case (_L', l') of + (VRecord xLs', _) -> return (Left xLs') + + (VConst cL, VRecord xLs') -> return (Right (cL, xLs')) + _ -> do let _L'' = quote names _L' @@ -822,9 +823,12 @@ infer typer = loop 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 + (Left _, VRecord xRs', _) -> + return (Left xRs') + + (Right _, VConst cR, VRecord xRs') -> return (Right (cR, xRs')) _ -> do let _R'' = quote names _R' @@ -832,7 +836,7 @@ infer typer = loop case mk of Nothing -> die (MustCombineARecord '∧' r'' _R'') Just t -> die (InvalidDuplicateField t r _R'') --- TODO examine why this `combineTypes` is different from that defined in `CombineTypes _ l r`. + let combineTypes xs xLs₀' xRs₀' = do let combine x (VRecord xLs₁') (VRecord xRs₁') = combineTypes (x : xs) xLs₁' xRs₁' @@ -849,7 +853,26 @@ infer typer = loop 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 + (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 From f7c03e3ba3bc347457a95a18d779b7685a53f669 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 14 Mar 2025 10:55:12 +0100 Subject: [PATCH 05/10] undo the formatting change because tests fail --- dhall/src/Dhall/Pretty/Internal.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index 4b9c7b305..fdd545d3c 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -432,7 +432,8 @@ combine ASCII = "/\\" combine Unicode = "∧" combineTypes :: CharacterSet -> Text -combineTypes = combine -- Replace //\\ by /\ as //\\ is now deprecated. +combineTypes ASCII = "//\\\\" +combineTypes Unicode = "⩓" prefer :: CharacterSet -> Text prefer ASCII = "//" From d21abae2a7b02c4c203e7dca4771029bfa988278 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 14 Mar 2025 11:56:41 +0100 Subject: [PATCH 06/10] implement /\ reduction for record types --- dhall/src/Dhall/Eval.hs | 6 ++++++ dhall/src/Dhall/Normalize.hs | 13 +++++++++---- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 73ba65b7a..c0ff76cc6 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -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' diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index c51377dfd..b8610b328 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -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 From be4ea3964069e0444cff3c1b30209bb3b9e0fcf8 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 14 Mar 2025 12:22:06 +0100 Subject: [PATCH 07/10] fix isNormalized --- dhall/src/Dhall/Normalize.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index b8610b328..e17d4859e 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -954,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 From 11a7b3cb3ef45212de5f1e848e4f09099671a90e Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Mon, 17 Mar 2025 17:48:31 +0100 Subject: [PATCH 08/10] add comment --- dhall/src/Dhall/TypeCheck.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 8df8b9bf2..c64bd7976 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -83,6 +83,7 @@ import qualified Dhall.Syntax as Syntax import qualified Dhall.Util import qualified Prettyprinter as Pretty import qualified Prettyprinter.Render.String as Pretty +import qualified Data.Type.Bool as types {-| A type synonym for `Void` @@ -811,6 +812,10 @@ infer typer = loop 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') From 8050d24e226fc93c72d5483a8b39b76d4f882a25 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Mon, 17 Mar 2025 18:10:02 +0100 Subject: [PATCH 09/10] remove wrong import --- dhall/src/Dhall/TypeCheck.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index c64bd7976..efa07f064 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -83,7 +83,6 @@ import qualified Dhall.Syntax as Syntax import qualified Dhall.Util import qualified Prettyprinter as Pretty import qualified Prettyprinter.Render.String as Pretty -import qualified Data.Type.Bool as types {-| A type synonym for `Void` From 8fe9623e98154df4d43c282e9ff9bf4254c79e7c Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 20 Mar 2025 22:29:00 +0100 Subject: [PATCH 10/10] refactor code for clarity --- dhall/src/Dhall/TypeCheck.hs | 67 +++++++++++++++++------------------- 1 file changed, 31 insertions(+), 36 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index efa07f064..792d56f53 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -801,46 +801,22 @@ infer typer = loop Combine _ mk l r -> do _L' <- loop ctx l + let _L'' = quote names _L' + let l' = eval values l let l'' = quote names l' _R' <- loop ctx r + let _R'' = quote names _R' + let r' = eval values r 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' - - case mk of - Nothing -> die (MustCombineARecord '∧' l'' _L'') - Just t -> die (InvalidDuplicateField t l _L'') - - -- Make sure both are on the Left (both record values) or on the Right (both record types). - rightTypeOrRecord <- case (leftTypeOrRecord, _R', r') of - (Left _, VRecord xRs', _) -> - return (Left xRs') - - (Right _, VConst cR, VRecord xRs') -> return (Right (cR, xRs')) - - _ -> do - let _R'' = quote names _R' - - case mk of - Nothing -> die (MustCombineARecord '∧' r'' _R'') - Just t -> die (InvalidDuplicateField t r _R'') - + -- 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₁' @@ -869,13 +845,32 @@ infer typer = loop Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) - case (leftTypeOrRecord, rightTypeOrRecord) of - (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) + -- 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 + (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