3 ms·

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 rea

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 "+"
        dmitriid 5y ago
        > 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." What is the value of adding this to types then? Besides increasing compilation time? > For the examples, you need {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} import GHC.TypeLits; type AddTest = 2 + 2 ~ 4 main.hs:5:20: error: * Expected kind `Nat', but `2 ~ 4' has kind `Constraint' * In the second argument of `(+)', namely `2 ~ 4' In the type `2 + 2 ~ 4' In the type declaration for `AddTest' | 5 | type AddTest = 2 + 2 ~ 4 | ^^^^^ exit status 1 So far "easily check type-level computation as well" fails to be easy.

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 "+"
        dmitriid 5y ago
        > 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." What is the value of adding this to types then? Besides increasing compilation time? > For the examples, you need {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} import GHC.TypeLits; type AddTest = 2 + 2 ~ 4 main.hs:5:20: error: * Expected kind `Nat', but `2 ~ 4' has kind `Constraint' * In the second argument of `(+)', namely `2 ~ 4' In the type `2 + 2 ~ 4' In the type declaration for `AddTest' | 5 | type AddTest = 2 + 2 ~ 4 | ^^^^^ exit status 1 So far "easily check type-level computation as well" fails to be easy.