Dhall-haskell: dhall-to-json None value not supported for optionals.

[andrewchambers]

 $ dhall-to-json <<< "Some 1"
1
$  dhall-to-json <<< "None"
Error: Cannot translate to JSON

[andrewchambers]

Not exactly sure what the best approach is, but it would be nice for my go package that uses dhall-to-json to be able to use optionals.

[singpolyma]

$ dhall-to-json <<< "None"

I believe you want something like None Natural -- the type is required.

[andrewchambers]

My mistake :)

[Profpatsch]

@singpolyma The way None works in the AST, you could also make None valid by itself, no?

[singpolyma]

‎> @singpolyma The way None works in the AST, you could also make None valid by itself, no?

By itself it is valid -- it's a function from a type to the empty optional of that type.‎

[Profpatsch]

By itself it is valid -- it's a function from a type to the empty optional of that type.‎

I know, but the AST doesn’t express that fact, so you could re-interpret it. Admittedly that would be a crude hack and go against dhall semantics.

Alternatively, a better error message would help. :P

[Gabriel439]

I don't think we should translate a bare None to null, but a better error message would be very easy to add. I will reopen this and make that the scope of this issue

[Gabriel439]

The fix is up here: https://github.com/dhall-lang/dhall-haskell/pull/895

[antislava]

Sorry for the late comment but it might clarify things a bit for some of us: None is technically a function taking a type as its argument:

$ dhall --annotate <<< 'None'                                                                  
None : ∀(A : Type) → Optional A

$ dhall --annotate <<< 'None Integer'                                                          
None Integer : Optional Integer

In other words, it is actually somewhat different from Nothing in Haskell, so that e.g. None : Optional Integer doesn't make sense (while Some +1 : Optional Integer does!).

[Gabriel439]

@antislava: Here is the new error message from the pull request that I have out for this:

$ dhall-to-json <<< 'None'

Error: A bare ❰None❱ is not valid                                          

Explanation: The conversion to JSON/YAML does not accept ❰None❱ in isolation as 
a valid way to represent ❰null❱.  In Dhall, ❰None❱ is a function whose input is 
a type and whose output is an absent value of that type.                        

For example:                                                                    


    ┌─────────────────────────────────┐  This is a function whose result is an  
    │ None : ∀(a : Type) → Optional a │  ❰Optional❱ value, but the function     
    └─────────────────────────────────┘  itself is not a valid ❰Optional❱ value 


    ┌─────────────────────────────────┐                                         
    │ None Natural : Optional Natural │  This is a valid ❰Optional❱ value (an   
    └─────────────────────────────────┘  absent ❰Natural❱ number in this case)  


The conversion to JSON/YAML only translates the latter form to ❰null❱.