Usage of reifyInt

[paulvictor]

Hello Bodil,

Can you please include an example of how to use reifyInt? It's not clear(for me atleast) what to use for the second argument.

Thanks Paul

[m-bock]

one year later... there's still no example that can be found on the web. Would be super nice to get some clarification about this function...

[mrgriffin]

You have to pass a function with type forall n. Nat n => n -> r, the r can be anything you like (i.e. it doesn't have to be polymorphic). For example you could pass toInt and get a pointless function that converts an Int into a Nat and back again.

> reifyInt 3 toInt
3
> reifyInt (-1) toInt
Error: reifyInt: integral < 0

Note that this second example is pretty sketchy because you have to prove to yourself that the Int is a valid Nat, I'd have liked to see reifyInt :: forall r. Int -> (forall n. Nat n => n -> r) -> Maybe r, or a Partial constraint.

Basically the idea is to use continuation-passing style so that we can process every Nat and convert them back into some common type r so that the rest of the program doesn't have to worry about which specific Nat type was chosen.

For a marginally more useful example you can call replicate from Data.Vec, but you're then forced to immediately process it because otherwise the unknown type would escape its scope:

> import Data.Vec
> reifyInt 1 (\n -> replicate n 'a')
The type variable n, bound at
  ...
has escaped its scope, appearing in the type
  Vec n0 Char
> reifyInt 1 (\n -> toArray $ replicate n 'a')
['a']

Of course you'd want to do something more interesting than toArray where the Nat was actually useful, but I can't think of anything off the top of my head. If there was some way to specify additional constraints that had to apply to the Nat then I can think of a use: smart constructors.

-- | Percentage type that contains an Int between 0 and 100 inclusive.
newtype Percentage = Percentage Int

-- | Constructs a Percentage whose validity is determined at compile-time.
natToPercentage :: forall n. Nat n => LtEq n D100 => n -> Percentage
natToPercentage = Percentage <<< toInt

-- | Reifies an Int known to be less than or equal to another Int.
-- NOTE: I am using the Maybe signature proposed above.
reifyLtEqInt :: forall r m. Nat m => m -> Int -> (forall n. Nat n => LtEq n m => r) -> Maybe r
reifyLtEqInt = undefined -- XXX: Obviously some code has to go here!

-- NOTE: Necessary because although D100 exists, d100 doesn't!
d100 :: D100
d100 = undefined

-- | Safely converts an Int into a Percentage.
intToPercentage :: Int -> Maybe Percentage
intToPercentage i = reifyLtEqInt d100 i natToPercentage