[Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers

[Richard Eisenberg]

Hi TP,

Here is slightly edited code that works:

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE StandaloneDeriving #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> 
> -- type level integers
> data Nat = Zero | Succ Nat
>    deriving ( Show, Eq, Ord )
> 
> -- Singleton allowing a correspondance between type-level and value-level
> -- integers.
> data SNat :: Nat -> * where
>    SZero :: SNat Zero
>    SSucc :: SNat n -> SNat (Succ n)
> deriving instance Show (SNat n)
> 
> data Proxy :: Nat -> * where
>    P     :: Proxy n
> deriving instance Show (Proxy n)
> 
> class MkSNat (n::Nat) where
>    mkSNat :: Proxy n -> SNat n
> 
> instance MkSNat Zero where
>    mkSNat _ = SZero
> 
> instance MkSNat n => MkSNat (Succ n) where
>    mkSNat _ = SSucc (mkSNat (P :: Proxy n))
> 
> main = do
> 
> let one = undefined :: Proxy ('Succ 'Zero)
> -- can't do the next line: one is undefined
> -- print one
> print $ mkSNat one

- I added the extension ScopedTypeVariables, which allows method definitions to access type variables from an instance header.

- I removed the problematic argument to P, as you don't need it.

- I changed the syntax of creating proxies. Instead of passing an argument, as you were trying, you set the type of a proxy using an explicit type annotation.

- I changed the pattern-match in mkSNat (in the Succ instance) to be _, as otherwise you end up pattern-matching on undefined in main.

- I added a Show instance for Proxy.

- I added an extra constraint to the Succ instance for MkSNat, requiring that n is in the MkSNat class, as well.

- I removed the line printing out the proxy, as it is undefined. If you replace `undefined` with `P` in the first line of main, you can print that out just fine.

I'm hoping that gets you moving again and seeing this helps you piece it all together.

And now, just a little theory: You can't really do what you want, and for good reason. You want a function (magic :: Nat -> SNat n). But, the type (SNat n) exposes the value of n to compile-time, type-level reasoning. For example, if a function only works on values other than 0, you could define that function with the signature (frob :: SNat (Succ n) -> Whatever). With that signature, you can't call frob with SZero. Say a program asks a user to input a Nat (using some input mechanism) and then you magically turn that Nat into an SNat n. Could you call frob with it? There's no way to know, because we can't possibly know what the value of n is at compile time. Thus, there are not many useful things you could do with such an SNat, whose index n is completely unknowable -- you might as well just use a Nat. Besides, there's no way to write the `magic` function, anyway.

But, say you really really want the `magic` function. Instead, you could do this:

> data ENat :: * where -- "existential SNat"
>   Exists :: SNat n -> ENat
> 
> mkENat :: Nat -> ENat
> mkENat Zero = Exists SZero
> mkENat (Succ n) = case mkENat n of Exists n' -> Exists (SSucc n')

The datatype ENat does *not* expose the type variable n; instead, that type variable is existential, and you can access it only by unpacking the existential with a case statement. These existentials are awkward to work with, but they're really the only solution to the problem you're bringing up. You can see some of this awkwardness in the second clause of mkENat. (And, yes, you really need `case`, not `let`. For a little fun, try replacing the RHS of that clause with this: `let Exists n' = mkENat n in Exists (SSucc n')`.) The reason that existentials are needed is that, in an existential, it's abundantly clear that it is impossible to know anything about the type index at compile-time -- which is exactly the case you're in.

Happy hacking,
Richard

On Jun 9, 2013, at 11:39 AM, TP wrote:

> Hi all,
> 
> Following a discussion on Haskell-Cafe, Richard E. made the following 
> proposition of a "Singleton" to make a correspondance between type-level 
> integers and value-level integers:
> 
> """
>> data SNat :: Nat -> * where
>>  SZero :: SNat 'Zero
>>  SSucc :: SNat n -> SNat ('Succ n) 
> """
> 
> (found at [1], and an example of application can be found at [2], also 
> proposed by Richard E.)
> 
> Now I asked myself if there is some means to write a function that would 
> take any value of type e.g. `Succ (Succ Zero)`, and would return the value 
> `SSucc (SSucc SZero)`.
> 
> I have tried hard, but did not succeed (see below). I am constantly 
> refrained by the fact a function or data constructor cannot take a value of 
> type having a kind different from `*` (if I am right).
> 
> Is there any solution to this problem?
> 
> Below is my attempt, which yields a compilation error
> 
> test_typeinteger_valueinteger_conversion.hs:18:14:
>    Expected a type, but ‛n’ has kind ‛Nat’
>    In the type ‛(n :: Nat)’
>    In the definition of data constructor ‛P’
>    In the data declaration for ‛Proxy’
> 
> ----------------------
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE StandaloneDeriving #-}
> 
> -- type level integers
> data Nat = Zero | Succ Nat
>    deriving ( Show, Eq, Ord )
> 
> -- Singleton allowing a correspondance between type-level and value-level
> -- integers.
> data SNat :: Nat -> * where
>    SZero :: SNat Zero
>    SSucc :: SNat n -> SNat (Succ n)
> deriving instance Show (SNat n)
> 
> data Proxy :: Nat -> * where
>    P     :: (n::Nat) -> Proxy n
> 
> class MkSNat (n::Nat) where
>    mkSNat :: Proxy n -> SNat n
> 
> instance MkSNat Zero where
>    mkSNat _ = SZero
> 
> instance MkSNat (Succ n) where
>    mkSNat (P (Succ n)) = SSucc (mkSNat (P n))
> 
> main = do
> 
> let one = undefined :: Proxy ('Succ 'Zero)
> print one
> print $ mkSNat (P one)
> ----------------------
> 
> Thanks,
> 
> TP
> 
> 
> References:
> -----------
> [1]: https://groups.google.com/forum/?fromgroups#!topic/haskell-cafe/mGDhPqHZAz8
> [2]: https://groups.google.com/d/msg/haskell-cafe/Rh65kdPkX70/T2zZpV6ZpjoJ
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>