Handle read at user-defined types
#2223
Labels
Z-Feature
A new feature to be added to the game.
Comments
mergify bot
pushed a commit
that referenced
this issue
Dec 26, 2024
Towards #116. This PR introduces a new built-in command `read`, which can (attempt to) convert text into values, *i.e.* a partial inverse to `format`. It has type `read : Text -> a` and is a little bit magical, since its behavior depends on the inferred output type. In particular, if reading at the expected output type succeeds, it will return the value read; otherwise it throws an exception. In other words, in order to use `read` successfully you must already know what type you expect to get. At first I gave it the type `Text -> (Unit + a)` and had it return `inl ()` whenever it failed, but then I realized that (1) you can make either version from the other (to convert `Text -> (Unit + a)` to `Text -> a`, `case` on the result and call `fail` if you get `inl`; to convert the other way, use `try`), but (2) it is simpler/easier to have the version that crashes to start and then use a `net` to turn it into the pure functional version if you wish, rather than the other way around (which requires a much harder-to-obtain `ADT calculator`). From a technical point of view, the way this is achieved is by inserting the type inferred for `read` as an extra parameter during elaboration. (Having types-as-special-values in the language might be useful for other things down the road as well.) Note that this makes `read` strictly weaker than the `read` function in Haskell, which works via dictionary-passing. For `read` in Swarm to work, its concrete type must be statically known at compile time. For example here is a function that works in Haskell but not Swarm: ``` def testRead : a -> Bool = \x. read (format x) == x end ``` I think it should still be sufficiently usable, however, and the current implementation is much simpler than going to full-fledged type classes. Currently `read` does not work on functions or delay types (even though such things are supported by `format`). We may add them in the future, but it would be much more complex since it would require parsing arbitrary Swarm code and dealing properly with environments and closures etc. `read` also does not currently work with user-defined types; see #2223 .
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Currently, the
readcommand (#2224) cannot handle user-defined types. For example,Fundamentally, the problem is that at runtime we no longer have easy access to tydefs that are in scope, so when we encounter a user-defined type like
Numwe don't know what it should expand to. There are two ways we could potentially solve this: (1) we could keep track of in-scope tydefs at runtime (maybe we already do this somewhere? I forget, but even if so it would still need to be plumbed through to where we executeread), or (2) we could expand away any user-defined types in the type ofreadprior to runtime, e.g. at typechecking or elaboration time. However, in that case we have to be careful to use the correct tydefs that are actually in scope.The text was updated successfully, but these errors were encountered: