Liquid Haskell might require you to prove that the divisor is nonzero, but even in standard Haskell there's common idioms for ensuring that a list is non-empty (data NonEmpty a = a :| [a]) or that text is non-empty (newtype NonEmptyText = NonEmptyText Text, with non-exported constructor, helpers like make :: Text -> NonEmptyText, or more advanced tricks like https://exploring-better-ways.bellroy.com/haskell-koan-type-... ).

The big problem preventing this approach from working for numbers is that it's just so cumbersome there. Most of this is because all the arithmetic operators are bundled into a single Num typeclass, and `fromInteger :: Num a => Integer -> a` has a type that's impossible for a "non-zero number" wrapper to satisfy.

▲ black_knight 5 hours ago | parent | next [-]

Definitely room for improvement on Haskell's standard library when it comes to the number-related type classes. Modern Haskell could do very well in this area with a good type-class redesign in this area. The issue I think is that this would invalidate a lot of existing code, relying upon that. But you can already replace Prelude with something else in your own code if you want to.

	▲	rootnod3 an hour ago \| parent [-]
		I think Idris has a better chance there.

▲ inigyou 5 hours ago | parent | prev [-]

OOP has those too, and they're very annoying.

▲ nh2 5 hours ago | parent [-]

In Haskell they are a little less annoying. It is just easier to reason about (including proving) pure functions.

▲ inigyou 5 hours ago | parent [-]

I meant the constrained types by hiding the constructors. Super annoying, not automatically convertible, in Haskell you have to remember what the fake constructor is called, and write it every time you use it, but at least it's efficiently implemented with newtype, unlike the Java OOP version. Think about writing a value with several nested constrained types, like NonEmptyListOne (makeNonZeroNumber 42, 'h' `NonEmptyString` "ello world"). It's just really annoying.

▲ _jackdk_ 3 hours ago | parent [-]

The blog link I mentioned avoids this cost with literals, by providing using a required type argument to check the string length at compile time without TH. It requires a relatively recent GHC:

    make :: forall symbol -> (IsNonEmptySymbol symbol) => NonEmptyText

    type family IsNonEmptySymbol symbol :: Constraint where
      IsNonEmptySymbol "" = Unsatisfiable (Text "Expected a non-empty string")
      IsNonEmptySymbol _ = (()::Constraint) -- empty constraint is always satisfied