CODEWITHSUNDEEP
haskelltypes
Cjen1
Cjen1

Reputation: 1746

Constructing a Nat type

I'm currently learning about using Nat from GHC.TypeLits

I am trying to lift an integer to the type level for testing via these definitions:

type IntNat (t::Nat) = Int

incNat :: IntNat t -> IntNat (t + 1)
incNat n = n + 1

fromInt :: Int -> IntNat t
fromInt(0) = (0 :: IntNat 0)
fromInt(n) = incNat (fromInt(n-1))

four = fromInt 4

From my understanding this should result in:

four = 4 :: IntNat (Nat 4)

However I am getting:

four = 4 :: IntNat t

Where am I going wrong, is it just that fromInt is erasing the type information?

Upvotes: 1

Views: 242

Answers (1)

Thomas M. DuBuisson
Thomas M. DuBuisson

Reputation: 64740

Because you defined a type synonym, and not a newtype, the meaning is quite different than what you seem to think. Roughly, IntNat _ will unify with Int and thus any other IntNat _.

You can try this out by defining other intnats and see them unify in, say, a list:

*Main> let five = 5 :: IntNat 99
*Main> let xs = [four, five] :: [IntNat 42]
*Main> :t xs
xs :: [IntNat 42]

or using a single intnat:

*Main> let four' = four :: IntNat 1000
*Main> :t four'
four' :: IntNat 1000

Instead consider using a newtype, such as newtype IntNat (n :: Nat) = IN Int. You'd get an error like:

• Couldn't match type ‘t’ with ‘0’
  ‘t’ is a rigid type variable bound by
    the type signature for:
      fromInt :: forall (t :: Nat). Int -> IntNat t
    at so.hs:12:1-26
  Expected type: IntNat t
    Actual type: IntNat 0
• In the expression: IN 0 :: IntNat 0
  In an equation for ‘fromInt’: fromInt 0 = IN 0 :: IntNat 0
• Relevant bindings include
    fromInt :: Int -> IntNat t (bound at so.hs:13:1)

This is because t and 0 are not the same - t is universal not existential. The offending lines are:

fromInt :: Int -> IntNat t
fromInt 0 = 0 :: IntNat 0

forall t. t == 0 is a hard proof to write

Upvotes: 2

Related Questions