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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
TP
Reply | Threaded
Open this post in threaded view
|

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

TP
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
TP
Reply | Threaded
Open this post in threaded view
|

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

TP
> 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*)
--------------

and in the "main" part:

--------------
let vector = Tensor { order = mkSNat (P::Proxy order), name = "u" } ::
Tensor (Succ Zero)
print vector
---------------

then the line (*1*) makes mandatory to use the extension
ScopedTypeVariables. But I don't see the difference with your line:

---------------
instance MkSNat n => MkSNat ('Succ n) where
   mkSNat _ = SSucc (mkSNat (P :: Proxy n))
---------------

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

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

I understand why we are compelled to use a constraint here:

---------------
instance MkSNat n => MkSNat ('Succ n) where
   mkSNat _ = SSucc (mkSNat (P :: Proxy n))
---------------

My understanding is that we are compelled to put a constraint `MkSNat n`
because we cannot be sure that n (which is a type of kind Nat because type
constructor Succ takes a type of kind Nat as argument to make a concrete
type) is an instance of MkSNat because we are precisely defining this
instance.

However, why am I compelled to put a constraint in

---------------
instance MkSNat o => Show (Tensor o) where
    show Tensor { order = o, name = str } = str ++ " of order "
            ++ (show (mkSNat (P :: Proxy o)))  --- (*1*)
---------------
?
Indeed, we know that Tensor takes a type of kind Nat to make a concrete
type, so o is a type of kind Nat. And we have made `'Succ n` and `Zero`
instances of MkSNat; are we compelled to put a constraint because Haskell
makes the hypothesis that o could be another type of kind Nat different from
`'Succ n` and `Zero`? If yes, is it related to the sentence I have already
read: "Typeclasses are open"?

Thanks,

TP




_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
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 the type of ???), you can just put a `P` there, and GHC will do the right (and only possible) thing. So, 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 because 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.

>
> However, why am I compelled to put a constraint in
>
> ---------------
> instance MkSNat o => Show (Tensor o) where
>    show Tensor { order = o, name = str } = str ++ " of order "
>            ++ (show (mkSNat (P :: Proxy o)))  --- (*1*)
> ---------------
> ?


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:

2) Class constraints are *runtime* things. This piece was a complete surprise to me when I first saw it, but it makes wonderful sense. One important property of Haskell is that it supports what is called "type erasure". Though the types are indispensable at compile-time, we have no need for them at runtime and can operate much faster without them. So, after type checking everything, GHC throws out the types. A consequence of type erasure is that a running program cannot make a decision based on a type. But, this conflicts with common knowledge: class methods are chosen based on types! The answer is that class constraints are *not* types. When you put, say, a (Show a) constraint on a function, you are really putting on an extra, implicit parameter to that function. This implicit parameter is a data structure that contains (pointers to) the specific implementations of the Show methods of type `a`. Thus, when you call `show`, that call compiles to a lookup in that data structure for the correct method. These data structures are called "dictionaries".

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 dictionary for MkSNat, which, in turn, encodes the value of "o". In a very real way, MkSNat and SNat are *the same data structure*. MkSNats are implicit and SNats are explicit, but otherwise, they contain exactly the same data and have exactly the same structure.

And, no, this issue is unrelated to the openness of type classes.


Though I promised myself I wouldn't post about it again on this list, it's too germane to the discussion not to: You may be interested in the paper I co-wrote last year on singletons and their implementation in GHC. You can find the paper here: http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf   A lot of the issues that you're asking about are discussed there. And, in MkSNat, you've already reinvented some of what's in there (I called MkSNat "SingI", because it Introducces a singleton).

Richard
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
TP
Reply | Threaded
Open this post in threaded view
|

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

TP
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
> dictionary for MkSNat, which, in turn, encodes the value of "o". In a very
> real way, MkSNat and SNat are *the same data structure*. MkSNats are
> implicit and SNats are explicit, but otherwise, they contain exactly the
> same data and have exactly the same structure.

"Type erasure" is a very interesting thing I did not know.
But I am not sure to understand correctly the fact that class constraints
are runtime things and why (I know C so I know what is a pointer, but I
would need to go into the details). Anyway, if it is clear that GHC does not
induction, then I can accept without problem that I am compelled to indicate
the class constraint `MkSNat o =>` to GHC, such that the call of mkSNat on a
value `P` of type `Proxy o` is correct from a type point of view - I imagine
this is the way most people in Haskell community think about class
constraints (?).

> Though I promised myself I wouldn't post about it again on this list, it's
> too germane to the discussion not to: You may be interested in the paper I
> co-wrote last year on singletons and their implementation in GHC. You can
> find the paper here:
> http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf   A lot of
> the issues that you're asking about are discussed there. And, in MkSNat,
> you've already reinvented some of what's in there (I called MkSNat
> "SingI", because it Introducces a singleton).

I have read the beginning of the paper: very interesting. In particular the
inequality at type level may be interesting for what I have to code. I will
try to go on in the next days. In fact I already read about this possibility
last month, but I stopped rapidly because I found this:

http://hackage.haskell.org/trac/ghc/ticket/4385
http://hackage.haskell.org/trac/ghc/attachment/ticket/4385/Ticket.hs

The answer of diatchki is not so hopeful, this suggests that there is a
limit to computations at type-level.

In my home project, I could code everything with a simple constructor of
type `Tensor` (not `Tensor order`) and runtime checks, but encoding
information in types makes certainly the code shorter (even if more
difficult to read for many people) and safer, perhaps quicker if the runtime
checks take time (I have heard from a colleague that the runtime checks of
size when indexing a vector, case with which you deal at the beginning of
your paper, took a lot of time in one of his C++ program - it is interesting
to see how you dealt with this problem).
It is a lot of efforts for me to learn all these advanced Haskell techniques
that are not in textbooks, but I feel it is important: I try to summarize
all what I learn in a LyX file.

My hope is at the end to be able to code clean and efficient code in real
programs, instead of script-like Python code with so many errors at runtime
(this is what I do at work these days in a scientific computing company). I
think also that for serious programs (say, order of magnitude 10^4 lines),
it is necessary to have types (I would not use Haskell for a small script,
of course). I feel also, from my coding experience, that states are a real
problem in traditional C/C++/Python/... code, and I want to give a try with
Haskell, monads, perhaps arrows, reactive programming, etc. Very
interesting, but time-consuming. Still a long path to go for me.

Thanks,

TP


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe