6 ms·

People do this actually. There's even best-in-class-level support for this in Haskell and Scala already: https://hackage.haskell.org/package/should-not-typeche

• dmitriid 5y ago
  These two check that something doesn't type check. They don't really check the logic you've coded in your types (and which will type check). For example, a real-world situation from Turkey (looking at my check from Marks and Specner): goods from category 1 (clothes) have VAT of 8%, from category 2 have VAT of 18 % (plastic bag), and that if a person buys 2 items they get a 15% discount, and if they buy 3 items they get a 25% discount, and there are additional discounts on various goods. This will type check even if you code it as "if there is 1 item, do a 40% discount, and assign VAT of 2%".
  • whateveracct 5y ago
    You can test for things type checking just fine without special stuff. In Haskell type Test1 = TypeExpressionImTesting ~ ExpectedType Thus, you can also easily check type-level computation as well. A concrete example type AddTest = 2 + 2 ~ 4 ^ This is valid Haskell and will confirm the addition function does what you expect
    • dmitriid 5y ago
      Once again, that's not what I asking or talking about. If you write 2 + 2 ~ 5, all types will be correct (Int), but the function will be incorrect. So the question is: now you've coded significantly more difficult logic than adding two Ints together with types. How will you test that logic?
      • whateveracct 5y ago
        If you write 2 + 2 ~ 5, your build will fail because your assertion failed. You can test more complicated logic the same way, using ~ as a type-level "shouldBe" that allows you to write type-level unit tests for said complicated logic.
        • dmitriid 5y ago
          > If you write 2 + 2 ~ 5, your build will fail because your assertion failed. So ~ tests not only the expected type, but the expected return value, too?
          • dmitriid 5y ago
            Okay, I'll answer my own question: ~ is type equality. "A type context can include equality constraints of the form t1 ~ t2, which denote that the types t1 and t2 need to be the same." [1] So. My question remains. What's to stop me from coding invalid logic in my types? How do I test the logic? BTW, can't verify that "you can also easily check type-level computation as well." The example fails here https://replit.com/languages/haskell https://replit.com/languages/haskell {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} type AddTest = 2 + 2 ~ 4 main.hs:4:18: error: Not in scope: type constructor or class `+' | 4 | type AddTest = 2 + 2 ~ 4 | ^ exit status 1 [1] https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/equality-constraints.html https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_gui...
            • whateveracct 5y ago
              > My question remains. What's to stop me from coding invalid logic in my types? How do I test the logic? You test the logic the same way people have tested term-level logic for years. You say "this call to my function with these args results in this output." At the term-level, you typically use equality to implement assert. ~ gives you a type-level "assertEqual" with which to write the exact same sort of unit tests you can write at the term level. -- For the examples, you need to import GHC.TypeLits. It has the type family "+"