2 ms·

Another alternative is sharing the types of the various ASTs but using parameterization to distinguish the cases. To restore nice, concise types, use a bunch o

by Peaker 13y ago

Another alternative is sharing the types of the various ASTs but using parameterization to distinguish the cases. To restore nice, concise types, use a bunch of type synonyms. While this is slightly cumbersome, I much prefer it over partiality. Ideally, even this wouldn't be necessary, with structural records and variants that let you work with changing, precise types without having to declare a lot of duplicate types.

eli_gottlieb 13y ago
Well that's the issue: I want to distinguish otherwise-identical trees in which certain particular node cases are either allowed or disallowed. In Haskell, AFAIK, that's hard. In Scala, it just requires copying your code over and over again, but it's possible and you can even share some of the code. The other solution I'm thinking of in Scala (that doesn't involve Option[T].get, I mean) is to treat the properties I want "proven" as a set of methods over the data, built as a separate object or trait similar to how Scala represents type-class dictionaries. I can then write one data-structure that quantifies over the type of the proof-witness dictionary it stores as part of itself. So when, for example, I want a fully-instantiated AST with no remaining "holes" to be filled in by static checking, I could write a function that only works on AST[FullyInstantiated]. Functions that don't care about the proof-witness are quantified over it. It then takes a bunch of extra typing to construct the proof-witness instances, but when I'm doing that construction I will have the compiler statically checking that all types relied on by the witness are correct.
- tikhonj 13y ago
  If I understand you correctly, you want to have a type like data Foo a = Bar a | Baz a | Qux a and then also use a type like data Foo' a = Bar a | Baz a in certain places. For one, this sounds like a perfect use case for OCaml's polymorphic variants[1]. I've always liked that particular feature. Honestly, most of the time, it seems like OCaml is the only language doing sub-typing correctly, especially in regards to type inference. [1]: http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual006.html#toc36 http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual006.ht... Haskell does not have polymorphic variants, unfortunately. Happily, we can add them in as syntax sugar over multiparameter typeclasses[2]. The very first example in section 1.2 of this paper is particularly relevant here: they're showing how polymorphic variants make it easy to work with different kinds of ASTs. I don't think this is necessarily an immediately practical approach, but it's very interesting from a language design point of view. [2]: http://guppy.eng.kagawa-u.ac.jp/~kagawa/PVH/PolymorphicVariantsInHaskell.pdf http://guppy.eng.kagawa-u.ac.jp/~kagawa/PVH/PolymorphicVaria... Your last example sounds like a prime case for using GADTs[3] (along with data kinds). You could write a type something like: data Typed = Checked | Unchecked data AST ∷ Typed → ★ where Checked' ∷ Int → AST 'Checked Unchecked' ∷ Int → AST 'Unchecked Neutral ∷ Int → AST a Now you can easily write functions expecting unchecked terms, checked terms or both. These functions will have type-checked pattern matching--you will only be able to match on cases for the appropriate type. The compiler can also do exhaustiveness checking based on the type. That is, if you write the following function: checked ∷ AST 'Checked → Int checked (Checked' i) = i you will get a warning that you missed the Neutral pattern, but not the Unchecked' pattern. And if you do try to add the Unchecked' pattern, you will get a type error. [3]: http://www.haskell.org/ghc/docs/6.6/html/users_guide/gadt.html http://www.haskell.org/ghc/docs/6.6/html/users_guide/gadt.ht... This approach gives you relatively little syntactic overhead at the use site--the appropriate type is chosen based on the constructors you used. You also get nice type-safe pattern matching. I think it's a very good tool for this job. Perhaps you should consider using Haskell more one of these days ;).
  - eli_gottlieb 13y ago
    Actually, this is a perfect demonstration of why I don't use Haskell. How many compiler extensions did you just invoke to accomplish what I can do trivially and already in Scala? So far, GADTs and Data Kinds. GADTs fall out trivially in Scala's case-classes, and the primary improvement of data-kinds over my witness objects is the ability to do full inference and polymorphism using the Neutral case. Which I think I can actually do anyway just by declaring the polymorphism, or even using inclusion polymorphism on the witnesses to make Neutral a supertype of Checked and Unchecked (thus letting any function valid for Neutral ASTs operate trivially over both other kinds). Polymorphic variants are indeed the ideal solution here, the problem being that those require either OCaml or a vastly improved subtyping system. I'm very slowly getting the logic worked out for the vastly improved subtyping system as a side-research project that's been going for years (but really got proper this past November as I started learning more of the logic behind type-theory and thus being able to reason much better about what I'm doing). For now, my own language would probably use structural-extensions and witness objects to do something like this, since it doesn't operate using the Vastly Improved Subtyping System.
    - tikhonj 13y ago
      I don't see what's wrong with including language features as extensions rather than bundling them into the core language the way Scala does. Sure, you have to explicitly turn them on in your file, but that's trivial. In practice, it's really no different from importing a library. At the very least, the GADT approach is not hard in Haskell. I don't see how it's any more difficult than the Scala approach. If anything, it's more natural: this is exactly the sort of use case GADTs were designed for. The main advantage of using GADTs here is that they're simple and explicit. Sure, you could do the same thing with case classes, but it would be more awkward, and you'd really be rebuilding part of the same functionality yourself. You don't really have to use data kinds in my example, but it makes the code nicer because you explicitly limit the types you can use as flags to 'Checked and 'Unchecked. You could have just made Checked and Unchecked empty types and stayed with normal kinds; the data kind approach is simply more elegant. The GADT method also ensures that the pattern matching is always safe. It also preserves exhaustiveness checking, which is very nice. I'm not sure if the Scala approach can do this. Another advantage over using witness objects (assuming I understood your idea correctly) is that you do not introduce anything new at the value level. 'Checked and 'Unchecked are only ever types, so the actual AST ends up being exactly the same as before just with a different type. I think this is a boon to clarity and simplicity. It also means that the use-site of the AST type doesn't change very much, if at all. Really, the main idea is that this is very easy in Haskell, basically using a single simple abstraction: the GADT. Just being hidden behind a language extension does not magically make the concept any more complicated or difficult to use! As an aside, if you want polymorphic variants, I don't see any reason not to use OCaml. It's a very nice language, and gets sub-typing right. All without sacrificing type inference.

by Peaker 13y ago

eli_gottlieb 13y ago

Well that's the issue: I want to distinguish otherwise-identical trees in which certain particular node cases are either allowed or disallowed. In Haskell, AFAIK, that's hard. In Scala, it just requires copying your code over and over again, but it's possible and you can even share some of the code. The other solution I'm thinking of in Scala (that doesn't involve Option[T].get, I mean) is to treat the properties I want "proven" as a set of methods over the data, built as a separate object or trait similar to how Scala represents type-class dictionaries. I can then write one data-structure that quantifies over the type of the proof-witness dictionary it stores as part of itself. So when, for example, I want a fully-instantiated AST with no remaining "holes" to be filled in by static checking, I could write a function that only works on AST[FullyInstantiated]. Functions that don't care about the proof-witness are quantified over it. It then takes a bunch of extra typing to construct the proof-witness instances, but when I'm doing that construction I will have the compiler statically checking that all types relied on by the witness are correct.

tikhonj 13y ago
If I understand you correctly, you want to have a type like data Foo a = Bar a | Baz a | Qux a and then also use a type like data Foo' a = Bar a | Baz a in certain places. For one, this sounds like a perfect use case for OCaml's polymorphic variants[1]. I've always liked that particular feature. Honestly, most of the time, it seems like OCaml is the only language doing sub-typing correctly, especially in regards to type inference. [1]: http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual006.html#toc36 http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual006.ht... Haskell does not have polymorphic variants, unfortunately. Happily, we can add them in as syntax sugar over multiparameter typeclasses[2]. The very first example in section 1.2 of this paper is particularly relevant here: they're showing how polymorphic variants make it easy to work with different kinds of ASTs. I don't think this is necessarily an immediately practical approach, but it's very interesting from a language design point of view. [2]: http://guppy.eng.kagawa-u.ac.jp/~kagawa/PVH/PolymorphicVariantsInHaskell.pdf http://guppy.eng.kagawa-u.ac.jp/~kagawa/PVH/PolymorphicVaria... Your last example sounds like a prime case for using GADTs[3] (along with data kinds). You could write a type something like: data Typed = Checked | Unchecked data AST ∷ Typed → ★ where Checked' ∷ Int → AST 'Checked Unchecked' ∷ Int → AST 'Unchecked Neutral ∷ Int → AST a Now you can easily write functions expecting unchecked terms, checked terms or both. These functions will have type-checked pattern matching--you will only be able to match on cases for the appropriate type. The compiler can also do exhaustiveness checking based on the type. That is, if you write the following function: checked ∷ AST 'Checked → Int checked (Checked' i) = i you will get a warning that you missed the Neutral pattern, but not the Unchecked' pattern. And if you do try to add the Unchecked' pattern, you will get a type error. [3]: http://www.haskell.org/ghc/docs/6.6/html/users_guide/gadt.html http://www.haskell.org/ghc/docs/6.6/html/users_guide/gadt.ht... This approach gives you relatively little syntactic overhead at the use site--the appropriate type is chosen based on the constructors you used. You also get nice type-safe pattern matching. I think it's a very good tool for this job. Perhaps you should consider using Haskell more one of these days ;).
- eli_gottlieb 13y ago
  Actually, this is a perfect demonstration of why I don't use Haskell. How many compiler extensions did you just invoke to accomplish what I can do trivially and already in Scala? So far, GADTs and Data Kinds. GADTs fall out trivially in Scala's case-classes, and the primary improvement of data-kinds over my witness objects is the ability to do full inference and polymorphism using the Neutral case. Which I think I can actually do anyway just by declaring the polymorphism, or even using inclusion polymorphism on the witnesses to make Neutral a supertype of Checked and Unchecked (thus letting any function valid for Neutral ASTs operate trivially over both other kinds). Polymorphic variants are indeed the ideal solution here, the problem being that those require either OCaml or a vastly improved subtyping system. I'm very slowly getting the logic worked out for the vastly improved subtyping system as a side-research project that's been going for years (but really got proper this past November as I started learning more of the logic behind type-theory and thus being able to reason much better about what I'm doing). For now, my own language would probably use structural-extensions and witness objects to do something like this, since it doesn't operate using the Vastly Improved Subtyping System.
  - tikhonj 13y ago
    I don't see what's wrong with including language features as extensions rather than bundling them into the core language the way Scala does. Sure, you have to explicitly turn them on in your file, but that's trivial. In practice, it's really no different from importing a library. At the very least, the GADT approach is not hard in Haskell. I don't see how it's any more difficult than the Scala approach. If anything, it's more natural: this is exactly the sort of use case GADTs were designed for. The main advantage of using GADTs here is that they're simple and explicit. Sure, you could do the same thing with case classes, but it would be more awkward, and you'd really be rebuilding part of the same functionality yourself. You don't really have to use data kinds in my example, but it makes the code nicer because you explicitly limit the types you can use as flags to 'Checked and 'Unchecked. You could have just made Checked and Unchecked empty types and stayed with normal kinds; the data kind approach is simply more elegant. The GADT method also ensures that the pattern matching is always safe. It also preserves exhaustiveness checking, which is very nice. I'm not sure if the Scala approach can do this. Another advantage over using witness objects (assuming I understood your idea correctly) is that you do not introduce anything new at the value level. 'Checked and 'Unchecked are only ever types, so the actual AST ends up being exactly the same as before just with a different type. I think this is a boon to clarity and simplicity. It also means that the use-site of the AST type doesn't change very much, if at all. Really, the main idea is that this is very easy in Haskell, basically using a single simple abstraction: the GADT. Just being hidden behind a language extension does not magically make the concept any more complicated or difficult to use! As an aside, if you want polymorphic variants, I don't see any reason not to use OCaml. It's a very nice language, and gets sub-typing right. All without sacrificing type inference.