4 ms·

You can test for things type checking just fine without special stuff. In Haskell type Test1 = TypeExpressionImTesting ~ ExpectedType Thus, you can also e

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.
        dmitriid 5y ago
        Okay, I finally made it compile. Let's revisit: > whateveracct: A concrete example > whateveracct: type AddTest = 2 + 2 ~ 4 > dmitriid: If you write 2 + 2 ~ 5, all types will be correct (Int), but the function will be incorrect. > whateveracct: If you write 2 + 2 ~ 5, your build will fail because your assertion failed. Just pasted this into https://replit.com/languages/haskell https://replit.com/languages/haskell, and of course it passed {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators, ConstraintKinds, TypeFamilies #-} import GHC.TypeLits; type AddTest = (2 + 2) ~ 5 main = putStrLn "Hello, World!"
        tome 5y ago
        You haven't tested the type you wrote. `type AddTest = (2 + 2) ~ 5` compiles without error the same way `addTest = (2 + 2) == 5` would run without error. To test it, try, for example {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators, ConstraintKinds, TypeFamilies #-} {-# LANGUAGE RankNTypes #-} import GHC.TypeLits test :: ((2 + 2) ~ 5 => a) -> a test x = x main = putStrLn "Hello, World!" That will fail to compile. If you change the 5 to 4 then it will compile.

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.
      - dmitriid 5y ago
        Okay, I finally made it compile. Let's revisit: > whateveracct: A concrete example > whateveracct: type AddTest = 2 + 2 ~ 4 > dmitriid: If you write 2 + 2 ~ 5, all types will be correct (Int), but the function will be incorrect. > whateveracct: If you write 2 + 2 ~ 5, your build will fail because your assertion failed. Just pasted this into https://replit.com/languages/haskell https://replit.com/languages/haskell, and of course it passed {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators, ConstraintKinds, TypeFamilies #-} import GHC.TypeLits; type AddTest = (2 + 2) ~ 5 main = putStrLn "Hello, World!"
        tome 5y ago
        You haven't tested the type you wrote. `type AddTest = (2 + 2) ~ 5` compiles without error the same way `addTest = (2 + 2) == 5` would run without error. To test it, try, for example {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators, ConstraintKinds, TypeFamilies #-} {-# LANGUAGE RankNTypes #-} import GHC.TypeLits test :: ((2 + 2) ~ 5 => a) -> a test x = x main = putStrLn "Hello, World!" That will fail to compile. If you change the 5 to 4 then it will compile.