Join GitHub today
GitHub is home to over 36 million developers working together to host and review code, manage projects, and build software together.
Sign upImplement Optional/build with fusion #44
Conversation
Gabriel439
reviewed
May 1, 2017
|
This looks great! My main suggestion is to add two more test cases. See below |
| @@ -1130,6 +1141,22 @@ normalize e = case e of | |||
| App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0) | |||
| App NaturalEven (NaturalLit n) -> BoolLit (even n) | |||
| App NaturalOdd (NaturalLit n) -> BoolLit (odd n) | |||
| App (App OptionalBuild t) k | |||
| | check -> OptionalLit t (Data.Vector.fromList k') | |||
This comment has been minimized.
This comment has been minimized.
Gabriel439
May 1, 2017
Collaborator
Minor suggestion: instead of using Data.Vector.fromList here, you can have go build a Vector directly:
go (App (Var "Just") e') = pure e'
go (Var "Nothing") = empty| check0 _ = False | ||
|
|
||
| check1 just nothing (App (Var (V just' n)) _) = | ||
| just == just' && n == (if just == nothing then 1 else 0) |
This comment has been minimized.
This comment has been minimized.
Gabriel439
May 1, 2017
Collaborator
Related to your previous question: this is very similar to how the more efficient version of normalization would work. It's just that I wrote isNormalized long after I wrote normalize so I wrote isNormalized with more careful attention to performance
| typeWith _ OptionalBuild = do | ||
| return | ||
| (Pi "a" (Const Type) | ||
| (Pi "f" f (App Optional "a") ) ) |
This comment has been minimized.
This comment has been minimized.
Gabriel439
May 1, 2017
Collaborator
Minor suggestion: replace "f" with "_" for consistency with List/build so that it doesn't show up in the type
| where test label inp out = testCase label $ do | ||
| isNormalized (e inp) @?= False | ||
| normalize' (e inp) @?= out | ||
| e inp = (OptionalFold `App` Text `App` OptionalLit Text inp `App` |
This comment has been minimized.
This comment has been minimized.
Gabriel439
May 1, 2017
Collaborator
Clever use of infix App! That would make the normalization code a lot easier to read with fewer parentheses since you I believe can also pattern match on an infix constructor
| nothing = test "nothing" [] (NaturalLit 2) | ||
|
|
||
| optionalBuild :: TestTree | ||
| optionalBuild = testCase "Optional/build" $ do |
This comment has been minimized.
This comment has been minimized.
Gabriel439
May 1, 2017
Collaborator
There are two test cases worth adding to deal with common ways to implement build incorrectly. First, you want to test that shadowing is handled correctly:
Optional/build
Integer
(λ(optional : Type) → λ(x : Integer → optional) → λ(x : optional) → x@1 3)... and you also want to test that it correctly handles an irreducible build like this:
λ(id : ∀(a : Type) → a → a)
→ Optional/build
Integer
( λ(optional : type)
→ λ(just : Integer → optional)
→ λ(nothing : optional)
→ id optional (just 3)
)... where "correctly handles" means that it doesn't fail with an error and doesn't accidentally interpret it as a reducible build
markus1189
force-pushed the
markus1189:optional-build
branch
from
c44d3ee
to
4c98811
May 1, 2017
This comment has been minimized.
This comment has been minimized.
|
Thanks for the review. I addressed all of your points (tests all pass, yay!) (And yes you can use infix notation for pattern matching ;) ) |
Gabriel439
merged commit 32aa2a7
into
dhall-lang:master
May 1, 2017
1 check passed
This comment has been minimized.
This comment has been minimized.
|
Awesome! Thank you for contributing this :) |
markus1189 commentedMay 1, 2017
Finally got around to do this ;)
OptionalFold