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@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
