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)’ 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
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
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
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
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
participants (2)
-
Richard Eisenberg -
TP