4 ms·

If you use it a lot it's likely a bad sign. Either that you are not using the type system's power to its full extent, or that the type system is too weak. In H

by Peaker 13y ago

If you use it a lot it's likely a bad sign. Either that you are not using the type system's power to its full extent, or that the type system is too weak. In Haskell, use of fromJust is considered a code smell, and is of course sometimes justified. But pretty rarely.

eli_gottlieb 13y ago
Generally, I use it where I could duplicate an entire data type with additional knowledge of the possible types. So for example, "AST that has been type-specialized and therefore contains no polymorphic type variables" would be a different type from "raw AST" or "type-generalized AST". I actually did write the code that way the first time around. However, it ended up being a huge duplication of effort for a tiny amount of increased safety from type-checking. Literally, if I'm willing to move the checks of certain type-system-checkable properties to runtime this way, I can write 1/3 the actual lines of code. The ideal would be to have data structures that are polymorphic over proofs of their properties, allowing the type-system to consider "unchecked AST", "generalized AST" and "specialized AST" as the instantiation of the same basic "AST" data type over three different proofs (or lack of proofs).
- 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.

by Peaker 13y ago

eli_gottlieb 13y ago

Generally, I use it where I could duplicate an entire data type with additional knowledge of the possible types. So for example, "AST that has been type-specialized and therefore contains no polymorphic type variables" would be a different type from "raw AST" or "type-generalized AST". I actually did write the code that way the first time around. However, it ended up being a huge duplication of effort for a tiny amount of increased safety from type-checking. Literally, if I'm willing to move the checks of certain type-system-checkable properties to runtime this way, I can write 1/3 the actual lines of code. The ideal would be to have data structures that are polymorphic over proofs of their properties, allowing the type-system to consider "unchecked AST", "generalized AST" and "specialized AST" as the instantiation of the same basic "AST" data type over three different proofs (or lack of proofs).

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.