2 ms·
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
by 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 agoYou 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 agoThank you! This leaves only the question of cost vs benefits of these approaches :)
- whateveracct 5y agomaybe a type Test (c :: Constraint) = c => () is in order here ;) testTheObvious :: Test ((2 + 2) ~ 5) testTheObvious = ()
- tome 5y agoThat compiles though. You need to CPS the constraint as in my example above. This does the job: type Test (c :: Constraint) = forall a. (c => a) -> a testTheObvious :: Test ((2 + 2) ~ 5) testTheObvious = id