CODEWITHSUNDEEP
haskelltype-level-computation
rityzmon
rityzmon

Reputation: 1965

Type-Level Peano Numbers and UndecidableInstances

Following this tutorial, I have the following code:

{-# LANGUAGE DataKinds, TypeFamilies #-}

data Nat = Z | S Nat

type family   Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z     m = m
type instance Plus (S n) m = S (Plus n m)

So far so good. I know that DataKinds does auto promotion of types to kinds, and TypeFamilies enable type-level functions.

Then I add:

type family Mul (m :: Nat) (n :: Nat) :: Nat
type instance Mul Z     m = Z
type instance Mul (S n) m = Plus m (Mul n m)

Compiling gives me:

Nested type family application
  in the type family application: Plus m (Mul n m)
(Use UndecidableInstances to permit this)
In the type instance declaration for ‘Mul’

The name of this extension is scary. Some people say to avoid it, and explanations of this extension I've tried reading do not make sense to me.

Looking for a bit of help in understanding the error, why it is showing up in this example, what is the meaning of undecidable in this context and in what instances this extension is as scary as it sounds?

Upvotes: 3

Views: 199

Answers (2)

leftaroundabout
leftaroundabout

Reputation: 120711

UndecidableInstance is ok to use. Granted, you should always consider a moment whether something is really needed, or it would be more idiomatic to choose another path.

Luke makes the point that UndecidableInstances should not be used to implement superclassing. Well, that's true, but it doesn't really have much to do with undecidable instances – superclassing is just always a hack and pretty much backwards to the way abstractions should be designed.

It is IME not true, at least not anymore, that superclassing is the most common use of UndecidableInstances. There are plenty of things you can do with this extension enabled but not without. Most certainly, it can't be possible to impose a halting-proof condition if you actually want to do Turing-complete dependent typing at compile-time, which is basically what all the DataKinds fuzz is heading to.

So, don't worry too much; indeed you probably won't get around UndecidableInstances. As said by András Kovács, this extension is perfectly safe WRT correctness, the worst that can happen is a loop / error.

If that's too scary for your tastes, use a language that's designed up front as dependently-typed and total, i.e. Agda.

Upvotes: 2

András Kovács
András Kovács

Reputation: 30103

It's not really scary. It disables the (rather weak) GHC checks that try to ascertain that type family and instance definitions terminate. So, its worst case behavior is non-terminating type checking. However, most often we get error messages instead of actual looping, because loops often exceed stack limits in the type checker. We don't get unsafety, incoherence or any other property that may adversely affect program robustness or inference.

"Undecidable" is probably a stronger expression than warranted, since it only denotes that GHC can't decide whether a definition is terminating. In many cases it's GHC that's too weak for the job, and other compilers for dependent languages would be able to check termination without problem. With GHC, UndecidableInstances is often required for obviously terminating definitions too, in which cases its usage is quite justified.

Upvotes: 2

Related Questions