At compile time generate type level Nats for constraint checking

user_3143065 0
Viewed 82

I am trying to have the value of an integer value represented at the type level at compile time such that I can check it against some constraints.

I would like users of the DSL to not have to write something like:

five = inc $ inc $ inc $ inc $ inc $ zero

Hence what I've been trying to create is a function which elevates that value to the type level.

ie

fromInt :: Int -> repr n
fromInt n = __

This is what I have tried so far:

data Z
data S a

data IntNat a = IN Int

zero = (IN 0 :: IntNat Z)

inc :: IntNat a -> IntNat (S a)
inc (IN i) = (IN (i + 1))

fromInt :: Int -> IntNat a 
fromInt 0 = (IN 0 :: IntNat Z)
fromInt n = inc (fromInt (n - 1))

This however fails since I don't have a general enough representation of the IntNat, IntNat Z ~/~ IntNat S Z.

Is this approach generally flawed, or is it a case of needing to enclose S Z in a type family / type class?

The other classic example of this would be to generate a vector of a specific length when using type level length annotated vectors. That function should address the same problem that I am having.

haskell types
2 Answers

Since Haskell does not have dependent types, there’s no way to lift value-level Int to a type-level natural. Depending on your use case, you have several approximating options.

Use continuation passing style

{-# LANGUAGE Rank2Types #-}

fromInt :: Int -> (forall a. IntNat a -> r) -> r
fromInt 0 f = f zero
fromInt n f = fromInt (n - 1) (f . inc)

Use an existential type

{-# LANGUAGE ExistentialQuantification #-}

data AnyIntNat = forall n. AnyIntNat (IntNat n)

fromInt :: Int -> AnyIntNat
fromInt 0 = AnyIntNat zero
fromInt n =
  case fromInt (n - 1) of
    AnyIntNat m -> AnyIntNat (inc m)

Take advantage of the existing type-level literals

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleContexts,
  TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances
  #-}

import GHC.TypeLits

class GetIntNat n where
  getIntNat :: IntNat n

instance GetIntNat Z where
  getIntNat = zero

instance GetIntNat n => GetIntNat (S n) where
  getIntNat = inc getIntNat

type family Peano n where
  Peano 0 = Z
  Peano n = S (Peano (n - 1))

-- usage: fromNat @5
fromNat :: GetIntNat (Peano n) => IntNat (Peano n)
fromNat = getIntNat
user_1150300

I would like users of the DSL to not have to write something like:

five = inc $ inc $ inc $ inc $ inc $ zero

This is the sort of thing you could easily write a quasiquoter for, but in this case you can use GHC's support for type-level Nat literals, converting to your representation using type families (which are type-level functions).

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, UndecidableInstances  #-}
import GHC.TypeLits
import Data.Proxy

data Z
data S a

type family FromNat (n :: Nat) where
  FromNat 0 = Z
  FromNat n = S (FromNat (n - 1))

fromNat :: Proxy n -> Proxy (FromNat n)
fromNat _ = Proxy

You also get some things like type-level addition etc

*Main GHC.TypeLits Data.Proxy> :t fromNat (Proxy :: Proxy 5)
fromNat (Proxy :: Proxy 5) :: Proxy (S (S (S (S (S Z)))))
*Main GHC.TypeLits Data.Proxy> :t fromNat (Proxy :: Proxy (3 + 2))
fromNat (Proxy :: Proxy (3 + 2)) :: Proxy (S (S (S (S (S Z)))))

EDIT: Anders in first with an answer, but leaving this as an alternative implementation

user_1768410
Related