Add field for unions #9
Conversation
alexhumphreys
force-pushed
the
feat/union-field
branch
6 times, most recently
from
6e701f4 to
1ea653e
Compare
Idrall/Check.idr
Outdated
| aEquivUnion : (i : Integer) -> | ||
| Namespace -> List (FieldName, (Maybe (Expr Void))) -> | ||
| Namespace -> List (FieldName, (Maybe (Expr Void))) -> Bool | ||
| aEquivUnion i ns1 [] ns2 [] = True | ||
| aEquivUnion i ns1 ((k, Nothing) :: xs) ns2 ((k', Nothing) :: ys) = | ||
| k == k' && aEquivUnion i ns1 xs ns2 ys | ||
| aEquivUnion i ns1 ((k, Just v) :: xs) ns2 ((k', Just v') :: ys) = | ||
| k == k' && | ||
| aEquivHelper i ns1 v ns2 v' && | ||
| aEquivUnion i ns1 xs ns2 ys | ||
| aEquivUnion i ns1 _ ns2 _ = False |
There was a problem hiding this comment.
Hmm, so I'm not sure how dhall works, but we might have to be more careful here. Is <Foo: Int, Bar: String> the same type as <Bar: String, Foo: Int>. Some languages with these kind of types allow the order to be different, but still be "same" type.
There was a problem hiding this comment.
It's a SortedMap and keys should be unique (the check for which i haven't implemented yet now that I'm thinking about it), so I think the should be enough to check for alpha equivalence.
| let x = freshen (ctxNames ctx) (closureName bT) in do | ||
| b' <- evalClosure bT (VNeutral aT (NVar x)) | ||
| case i of | ||
| Prim => readBackTyped ctx b' (f VPrimVar) -- TODO double check b' here |
There was a problem hiding this comment.
Hmm... shouldn't we get back a lambda from this? Maybe we already do?
There was a problem hiding this comment.
Good question. Not sure exactly what this reads back to, or what values would cause this case to be hit, but it's pretty similar to Andras's version dhall-lang/dhall-haskell@627a6cd#diff-fb8fa4dd3e70181d66f30003f0f14a64f9ffb4d382266ddcf15746f09cd6ad91R776
line 753/776 of eval.hs
| readBackUnion : Ctx -> (FieldName, Maybe Value) -> Either Error (FieldName, Maybe (Expr Void)) | ||
| readBackUnion ctx (k, Nothing) = Right (k, Nothing) | ||
| readBackUnion ctx (k, Just v) = Right (k, Just !(readBackTyped ctx (VConst CType) v)) | ||
| -- TODO is (VConst CType) always right here ^^^? Looks like rBT ignores the Ty param when reading back VConsts so maybe? |
There was a problem hiding this comment.
I think it is fine, since you are only using it for the type
There was a problem hiding this comment.
Aye, was thinking so too. Andras's branch doesn't have a type param at all for reading back, not sure the implications of that, so I guess when reading back the straight forward type values (VType, VKind, VBool) should be safe to ignore that type param.
Idrall/Check.idr
Outdated
| b' <- synth ctx b | ||
| isTypeKindSort ctx b' | ||
| Right (k, Just b') | ||
| getHighestType : (acc : Either Error Ty) -> Maybe Ty -> Either Error Ty |
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Sometimes you need to compare VHPi and VPi directly like in the following case: ``` let x = < Foo : Natural >.Foo in let y = \(Foo : Natural) -> < Foo : Natural >.Foo Foo in let list = [x, y] in list ``` Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
alexhumphreys
force-pushed
the
feat/union-field
branch
from
1eb5ae8 to
d59c2f0
Compare
Added the
.(field) operator for unions. Depends on #8Commit
62a30beis an interesting on here. I addedVHLamandVHPifor handling fields. I thought I could get away with letting the parser handling union constructor with arguments, but that wouldn't handle the following case:So since the apply operator needed to know about field application, and I'd need to synth some complicated types, it seemed easier to add
VHLamandVHPi. My thinking is theVH*stuff is for built ins, or things constructed during type synthesis, andVLamandVPiare for actual lambdas found in the user provided dhall expressions. BothVPiandVHPiget read back asEPi, so the should be possible to compare.