TP | 9 Jun 12:39 2013
Picon

writing a function to make a correspondance between type-level integers and value-level integers

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)’
(Continue reading)

Richard Eisenberg | 9 Jun 14:33 2013

Re: writing a function to make a correspondance between type-level integers and value-level integers

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
(Continue reading)

TP | 9 Jun 23:20 2013
Picon

Re: writing a function to make a correspondance between type-level integers and value-level integers

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

Thanks a lot Richard,

It helped me a lot to move forward. No doubt your answer will be very useful 
for people looking for information on internet.

> - 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.

Indeed I did not realize that I could use `P::Proxy n`, and so that n does 
not need to be argument of the data constructor `P`. 

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

In fact the extension ScopedTypeVariables is not needed to make your version 
work. However, if I extend a bit your version like that:

-------------
data Tensor :: Nat -> * where
    Tensor :: { order :: SNat order, name :: String } -> Tensor order

instance MkSNat o => Show (Tensor o) where
    show Tensor { order = o, name = str } = str ++ " of order "
            ++ (show (mkSNat (P :: Proxy o)))  --- (*1*)
--------------

(Continue reading)

Richard Eisenberg | 10 Jun 00:09 2013

Re: writing a function to make a correspondance between type-level integers and value-level integers

More good questions.

On Jun 9, 2013, at 10:20 PM, TP wrote:

> In fact the extension ScopedTypeVariables is not needed to make your version 
> work. However, if I extend a bit your version like that:
> 
<snip>

> So I don't understand why ScopedTypeVariables is needed in one case and not 
> in the other.
> 

This is because my code was (unintentionally) slightly redundant.

Here is the relevant code:

instance MkSNat n => MkSNat (Succ n) where
   mkSNat _ = SSucc (mkSNat ???)

What could possibly go in `???`? As in, what is the required type of that expression? We know
mkSNat :: forall m. MkSNat m => Proxy m -> SNat m
and
SSucc :: forall m. SNat m -> SNat (Succ m)

Here, we are defining an instance of mkSNat where we know a bit more about its type. This instance of mkSNat
must have type (Proxy (Succ n) -> SNat (Succ n)). (I'm just substituting in the (Succ n) from the instance
header.) So, that means that the call to SSucc in the body of mkSNat must return a SNat (Succ n), which in turn
means that its argument (mkSNat ???) must have type SNat n. Thus, in turn, the argument to that mkSNat must
have type Proxy n. Because all of these inferences are sound and forced (i.e., there is no other choice for
(Continue reading)

TP | 11 Jun 00:37 2013
Picon

Re: writing a function to make a correspondance between type-level integers and value-level integers

Richard Eisenberg wrote:

> without ScopedTypeVariables, the n that you would put on your annotation
> is totally unrelated to the n in the instance header, but this is benign
> becau
>  se GHC can infer the type anyway. With ScopedTypeVariables, the `n`s are
>  the same, which luckily agrees with GHC's reasoning, so it's all OK.

Thanks Richard, it is perfectly clear.

> There are two good reasons:
> 
> 1) You are suggesting that GHC do the following analysis:
> - There is an instance for MkSNat Zero.
> - Given an instance for MkSNat n, we know there is an instance for MkSNat
> (Succ n). - Thus, there is an instance for every (n :: Nat).
> This is precisely the definition of mathematical induction. GHC does not
> do induction. This could, theoretically, be fixed, though, which brings us
> to reason #2:

Ok, I imagine there is no general need for induction in GHC, otherwise it 
would already be implemented.

> 2) Class constraints are *runtime* things. This piece was a complete
[...]
> In effect, when you put the "MkSNat o" constraint on your instance, you
> are saying that we must know the value of "o" at *runtime*. This makes
> great sense now, because we really do need to know that data at runtime,
> in order to print the value correctly. Thinking of dictionaries, the
> dictionary for Show for Tensors will contain a pointer to the correct
(Continue reading)


Gmane