[Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers
Well, I guess you might be interested in geometric algebra then http://dl.acm.org/citation.cfm?id=1173728 because Geometric Algebra is a quite more principled way of doing component-free calculations. See also the web page of the author http://staff.science.uva.nl/~fontijne/ Geigen seems like a nice DSL that could well be embedded in Haskell. Anyway, the reason I pointed out Vectro is that it answers your question about reifying and reflecting type-level integers (by means of a type class). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers
Thanks Oleg, I have discovered geometric algebra some months ago. There is a textbook on the topic: http://eu.wiley.com/WileyCDA/WileyTitle/productCd-0470941634.html It seems very interesting, but I have not currently the time to make a detailed comparison with vector/tensor algebra. Moreover I have not your level of knowledge in Haskell/Standard ML and type theory, so I have already a lot of work. However, for sure this is something I will do in the few next years, because I think that notations are very important in physics and mathematics: it is of huge interest to have a condensed and easy to remember notation; still better if it is easily extended to higher dimensions/orders (unfortunately, generally these notations are not taught at university). Regards, TP o...@okmij.org wrote: Well, I guess you might be interested in geometric algebra then http://dl.acm.org/citation.cfm?id=1173728 because Geometric Algebra is a quite more principled way of doing component-free calculations. See also the web page of the author http://staff.science.uva.nl/~fontijne/ Geigen seems like a nice DSL that could well be embedded in Haskell. Anyway, the reason I pointed out Vectro is that it answers your question about reifying and reflecting type-level integers (by means of a type class). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers
o...@okmij.org wrote: I'm late to this discussion and must have missed the motivation for it. Specifically, how is your goal, vector/tensor operations that are statically assured well-dimensioned differs from general well-dimensioned linear algebra, for which several solutions have been already offered. For example, the Vectro library has been described back in 2006: http://ofb.net/~frederik/vectro/draft-r2.pdf http://ofb.net/~frederik/vectro/ The paper also talks about reifying type-level integers to value-level integers, and reflecting them back. Recent GHC extensions (like DataKinds) make the code much prettier but don't fundamentally change the game. Thanks Oleg for pointing out to this library. For the time being, I'm interested in doing component-free computations: http://gs1.dlut.edu.cn/newVersion/Files/dsxx/610.pdf But this library (and the corresponding article) may help me in the future. Thanks, TP ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers
I'm late to this discussion and must have missed the motivation for it. Specifically, how is your goal, vector/tensor operations that are statically assured well-dimensioned differs from general well-dimensioned linear algebra, for which several solutions have been already offered. For example, the Vectro library has been described back in 2006: http://ofb.net/~frederik/vectro/draft-r2.pdf http://ofb.net/~frederik/vectro/ The paper also talks about reifying type-level integers to value-level integers, and reflecting them back. Recent GHC extensions (like DataKinds) make the code much prettier but don't fundamentally change the game. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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
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 #-}
{-#
Re: [Haskell-cafe] 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*)
--
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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
