[Haskell-cafe] parse error in pattern, and byte code interpreter

[TP]

Hi everybody,

I want to test a higher level language than C/C++ (type inference, garbage 
collection), but much faster than Python. So I am naturally led to Haskell or 
OCaml.

I have read and tested tutorials for the two languages. For the time being, my 
preference goes to Haskell, first because it looks more like Python, and also 
because some things appear not so clean in OCaml, at least for a beginner (Put 
a line termination or not? Why have I to put rec in the definition of a 
recursive function? Etc.).

I have two questions.

1/ Inspiring from tutorials out there, I have tried to write a small formal 
program which is able to distribute n*(x+y) to n*x+n*y. The OCaml version is 
working (see Post Scriptum). However, I have difficulties to make the Haskell 
version work. This is my code:

{}
data Expr = Plus Expr Expr
  | Minus Expr Expr
  | Times Expr Expr
  | Divide Expr Expr
  | Variable String
deriving ( Show, Eq )

expr_to_string expr = case expr of
Times expr1 expr2 - ( ++ ( expr_to_string expr1 ) ++  * 
++ ( expr_to_string expr2 ) ++ )
Plus expr1 expr2 - ( ++ ( expr_to_string expr1 ) ++  + 
++ ( expr_to_string expr2 ) ++ )
Variable var - var

distribute expr = case expr of
 Variable var - var
 Times expr1 Plus( expr2 expr3 ) -
 Plus ( Times ( expr1 expr2 ) Times ( expr1 expr3 ) )

main = do
let x = Times ( Variable n )
( Plus ( Variable x ) ( Variable y ) )
print x
print ( expr_to_string x )
{}

When I try to run this code with runghc, I obtain:

pattern_matching_example.hs:28:24: Parse error in pattern: expr2

Thus it does not like my pattern Times expr1 Plus( expr2 expr3 ). Why?
How can I obtain the right result, as with the OCaml code below?

2/ It seems there is no possibility to generate bytecode, contrary to OCaml. 
Is it correct? Is there an alternative?
What is interesting with bytecode run with ocamlrun is that the process of 
generating the bytecode is very fast, so it is very convenient to test the 
program being written, in an efficient workflow. Only at the end the program is 
compiled to get more execution speed.

Thanks a lot in advance.

TP

PS:
---
To test the OCaml tutorial, type:
$ ocamlc -o pattern_matching_example pattern_matching_example.ml
$ ocamlrun ./pattern_matching_example

(*)
(* from OCaml tutorial, section 'data_types_and_matching.html' *)

(* This is a binary tree *)
type expr = Plus of expr * expr
  | Minus of expr * expr
  | Times of expr * expr
  | Divide of expr * expr
  | Value of string
;;

let v = Times ( Value n, Plus (Value x, Value y) )

let rec to_string e =
match e with
Plus ( left, right ) - ( ^ (to_string left ) ^  +  ^ (to_string 
right) ^ )
  | Minus ( left, right ) - ( ^ (to_string left ) ^  -  ^ (to_string 
right) ^ )
  | Times ( left, right ) - ( ^ (to_string left ) ^  *  ^ (to_string 
right) ^ )
  | Divide ( left, right ) - ( ^ (to_string left ) ^  /  ^ (to_string 
right) ^ )
  | Value value - value
;;

(* by type inference, ocaml knows that e is of type expr just below *)
let print_expr e = print_endline ( to_string e );;

print_expr v;;

let rec distribute e =
match e with
Times ( e1, Plus( e2, e3 ) ) -
Plus (Times ( distribute e1, distribute e2 )
, Times ( distribute e1, distribute e3 ) )
  | Times ( Plus( e1, e2 ), e3 ) -
Plus (Times ( distribute e1, distribute e3 )
, Times ( distribute e2, distribute e3 ) )
  | Plus ( left, right ) - Plus ( distribute left, distribute right )
  | Minus ( left, right ) - Minus ( distribute left, distribute right )
  | Times ( left, right ) - Times ( distribute left, distribute right )
  | Divide ( left, right ) - Divide ( distribute left, distribute right )
  | Value v - Value v
;;

print_expr ( distribute v );;
(*)

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] adding the elements of two lists

[TP]

Hello,

My primary problem may be reduced to adding elements of two lists:
[1,2,3] + [4,5,6] = [5,7,9]

My first idea was to declare a list of Int as an instance of Num, and define 
(+) 
in the correct way.
However, it seems it is not possible to do that:

---
instance Num [Int] where
l1 + l2 = 
---

Why?
It seems it is necessary to do:

--
newtype ListOfInt = ListOfInt { getList :: [Int] }
deriving (Show, Eq)

instance Num ListOfInt where
 l1 + l2 = ...
---

Am I correct? Is it the best way to do that?

Now, what is the most usual way to implement l1+l2?
I have just read about applicative functors, with which I can do:

---
import Control.Applicative
let l1 = [1,2,3]
let l2 = [4,5,6]
print $ getZipList $ (+) $ ZipList l1 * ZipList l2
[5,7,9]
---

Is it the correct way to do that?
I have tried:

---
instance Num ListOfInt where
 l1 + l2 = ListOfInt $ getZipList $ (+) $ ZipList (getList l1) *
 ZipList (getList l2)
---

Isn't it too much complicated?

Thanks

TP

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] get a string representation (show) of a function argument

[TP]

Hi,

I don't known the advanced features and extensions of GHC at all.

Look at the following program:

f :: Integer - Integer - IO Integer
f a b = do
print $ first argument= ++ (show a)
print $ second argument= ++ (show b)
print $ a+b
return (a+b)

main = do
k - f 3 5
f 2 k


It yields:

first argument=3
second argument=5
8
first argument=2
second argument=8
10
10


I am wondering if there is any means to get f 3 5 instead of 8 in the 
output of this program.
My idea would be to write some generic test function: I give it an expression 
(probably a function call) and the expected result (as a string), and then:

* it should check that the obtained result is identical to the expected one.

* it should also print the expression that yielded the first argument of the 
test function (i.e. the function call), under an understandable form (show). 
This is the feature that is missing to my mind in some test suites: for 
example in HUnit, it is not automatic: in the first argument of assertEqual, we 
may give a string corresponding to the executed command, see the documentation 
of Test.HUnit:

test1 = TestCase (assertEqual for (foo 3), (1,2) (foo 3))
 runTestTT tests
# Failure in: 0:test1
for (foo 3),
expected: (1,2)
 but got: (1,3)
Cases: 2  Tried: 2  Errors: 0  Failures: 1
So, we have duplication of code: foo 3.
On the other hand, I guess that the needed features to do that are not 
possible in Haskell (related to some kind of metaprogramming), but I prefer to 
ask people about that.

Thanks in advance,

TP___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] using FlexibleInstances and OverlappingInstances

[TP]

Hello,

In a module I am writing, I would like to use FlexibleInstances and 
OverlappingInstances.
But I get errors, so I am trying to reproduce the problems on a smaller 
program:


{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

data Foo = Foo Int
deriving ( Show )

instance Show [Foo] where
show [] = [0]
show l  = map show l

main = do
let l = [ Foo 1, Foo 2 ]
print l


The first error I obtain is:

test_overlappinginstances.hs:7:19:
Couldn't match expected type `Char' with actual type `[Char]'
Expected type: a0 - Char
  Actual type: a0 - String
In the first argument of `map', namely `show'
In the expression: map show l


Where does this Char come from? How to solve this problem?

The second error is:

test_overlappinginstances.hs:11:5:
Overlapping instances for Show [Foo]
  arising from a use of `print'
Matching instances:
  instance Show a = Show [a] -- Defined in GHC.Show
  instance [overlap ok] Show [Foo]
-- Defined at test_overlappinginstances.hs:5:10-19


The overlap is ok (overlap ok does not appear if not using the pragma 
OverlappingInstances), so it should work?

Thanks in advance,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] using FlexibleInstances and OverlappingInstances

[TP]

On Saturday 07 April 2012 14:22:15 you wrote:
 Is your actual issue with Showing a list? If so, you might be better
 off using the 'showList' member of the 'Show' typeclass:
 
 instance Show Foo where
show x = ...
showList xs = ...
 
 Then your 'showList' method will be called when 'show' is called on a
 list of 'Foo' values.

Yes, my problem is to show a list. Thanks a lot. Your solution should work in 
my more complicated module. I have modified the simple program of my post to 
make it work with showList as you advised:

data Foo = Foo Int

instance Show Foo where
show (Foo i) = show i

-- Implementation of showList found at:
-- http://www.haskell.org/pipermail/haskell-cafe/2010-May/077818.html
-- showList []   = showString []
-- showList (x:xs)   = showChar '[' . shows x . showl xs
--   where showl [] = showChar ']'
-- showl (x:xs) = showChar ',' . shows x . showl xs
--  So with the inspiration from above, I can create my implementation
--  in the accumulator style:
--  http://www.willamette.edu/~fruehr/haskell/evolution.html
--  Not a lot of information on Show instance. Haskell, the Craft of
--  functional programming quotes:
--  http://www.haskell.org/tutorial/stdclasses.html#sect8.3
-- Not a lot of information at:
-- http://book.realworldhaskell.org/read/using-typeclasses.html#id608052

showList [] = shows Empty list
showList (x:xs) = showChar '' . shows x . showl xs
where showl [] = showChar ''
  showl (x:xs) = showChar ';' . shows x . showl xs

main = do
print [ Foo 1, Foo 2]
print ([] :: [Foo])


 The first error is because 'map show l' is the wrong type - mapping
 show over a list will give you a list of strings, but 'show' must
 return a string. I think you could use 'concatMap' here.

Thanks. The first error was so stupid... Perhaps I was a little disturbed by 
overlapping instances.
 
 Other than that the only advice I can give is that I try my hardest to
 avoid OverlappingInstances.

I have found more information about overlapping instances at:

http://book.realworldhaskell.org/read/using-typeclasses.html#id608052

but it does not seem to work well; or it is rather tricky: I have been unable 
to make my initial post example work with overlapping instances. However, I 
don't see why it could not work.

Thanks

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] desactivate my Show instance implementations temporarily

[TP]

Hello,

I have a module where I have made several types as instances of the Show 
typeclass.

For debugging purpose, I would like to use the default implementation for Show 
(the one obtained when using deriving, which shows all the constructors). Is 
there some option to do that, or have I to comment all the Show instances of 
my code, and add Show in deriving (...) for each of my types? If this is 
the only possibility, is there some script around here to do that 
automatically?

Thanks in advance,

TP

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] desactivate my Show instance implementations temporarily

[TP]

On Sunday 22 April 2012 19:37:19 Ivan Lazar Miljenovic wrote:

 Is there any particular reason you're *not* using the defaults?

This is a good question which I have asked myself. I have searched about the 
topic, and found that:

http://blog.romanandreg.com/post/13545420287/haskells-show-and-pretty-
printing-bad-practice

So, according to this address, Show implementation should be used with Read so 
as to have show.read equal to identity: this is the only good practice 
requirement.

In my case, I use Show to print mathematical expressions, but it is not 
strictly pretty printing (not over several lines as in classical Computer 
Algebra Sytems). Why not using my own Show implementation to do that?

TP

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] phantom types

[TP]

Hi,

I am currently reading documentation on Generalized Algebraic Data Types:

http://en.wikibooks.org/wiki/Haskell/GADT

I have a question concerning this page. Let us consider the following code 
proposed in the page:

--
-- Phantom type variable a (does not appear in any Expr: it is just a
-- dummy variable).
data Expr a = I Int
| B Bool
| Add (Expr a) (Expr a)
| Mul (Expr a) (Expr a)
| Eq (Expr a) (Expr a)
deriving (Show)

-- Smart constructors
add :: Expr Int - Expr Int - Expr Int
add = Add

i :: Int  - Expr Int
i = I

b :: Bool - Expr Bool
b = B

eval :: Expr a - a
eval (I n) = n
--

I obtain the following error:

Phantom.hs:27:14:
Couldn't match type `a' with `Int'
  `a' is a rigid type variable bound by
  the type signature for eval :: Expr a - a at Phantom.hs:27:1
In the expression: n
In an equation for `eval': eval (I n) = n

The wiki page explains:


But alas, this does not work: how would the compiler know that encountering 
the constructor I means that a = Int?


I don't understand. When we write eval (I n) = n, as I is a constructor 
which takes an Int as argument, we are able to deduce that the type of n is 
Int; so the type of eval should be in this case Expr Int - Int.
What do I miss?

Thanks,

TP___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] phantom types

[TP]

First, thanks for your answer.

On Friday, August 17, 2012 15:31:32 you wrote:

 So if we define eval the way it is defined in the example, the
 compiler cannot infer that the type of (I n) is Expr Int, even though
 it knows that n's type is Int.

I think that my problem came from the fact that I have misunderstood type 
variables.

We have seen that the function eval:

eval :: Expr a - a
eval (I n) = n

yields a compilation error:


Phantom.hs:37:14:
Couldn't match type `a' with `Int'
`a' is a rigid type variable bound by
the type signature for eval :: Expr a - a


A somewhat similar error is found at 
http://stackoverflow.com/questions/4629883/rigid-type-variable-error

test :: Show s = s
test = asdasd

yields a compilation error:


Could not deduce (s ~ [Char])
from the context (Show s)
bound by the type signature for test :: Show s = s
at Phantom.hs:40:1-15
`s' is a rigid type variable bound by
the type signature for test :: Show s = s


Both errors contain the expression rigid type variable. The explanation in 
the Stack Overflow page made me understand my error:

test :: Show s = s means for any type s which is an instance of Show, test 
is a value of that type s.

Something like test :: Num a = a; test = 42 works because 42 can be a value 
of type Int or Integer or Float or anything else that is an instance of Num. 
However asdasd can't be an Int or anything else that is an instance of Show 
- it can only ever be a String. As a consequence it does not match the type 
Show s = s.

The compiler does not say: «s is of type String because the return type of 
test is a String».

Identically, in our case, «eval :: Expr a - a» means «for any type a, eval 
takes a value of type «Expr a» as input, and outputs a value of type a». 
Analogously to the above case, the compiler does not say «a is of type Int, 
because n is of type Int». 

The problem here is that (I n) does not allow to know the type of a. It may be 
of type Expr String as you have shown:

*Main let expr = I 5 :: Expr String
*Main expr
I 5
*Main :t expr
expr :: Expr String

So we may have anything for «a» in «Expr a» input type of eval. These 
multiplicity of values for «a» cannot match the output type of the equation 
«eval (I n) = n» which is an Int. Thus we get an error.

Am I correct?

Thanks,

TP

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] partially applied data constructor and corresponding type

[TP]

Hello,

I ask myself if there is a way to do the following.
Imagine that I have a dummy type:

data Tensor = TensorVar Int String

where the integer is the order, and the string is the name of the tensor.
I would like to make with the constructor TensorVar a type Vector, such 
that, in pseudo-language:

data Vector = TensorVar 1 String

Because a vector is a tensor of order 1.

Is this possible? I have tried type synonyms and newtypes without any success.

Thanks a lot,

TP

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] partially applied data constructor and corresponding type

[TP]

Thanks Yury,

The problem with this solution is that if I have written a method for the 
Tensor type (for example a method of a typeclass of which Tensor is an 
instance) that uses the order of the tensor (your ndims) in a general way, I 
cannot reuse it easily for a vector defined like that.

In fact, my problem is to be able to define:
* from my type Tensor, a type Vector, by specifying that the dimension 
must be one to have a Vector type.
* from my constructor TensorVar, a constructor VectorVar, which 
corresponds to TensorVar with the integer equal to 1.

The idea is to avoid duplicating code, by reusing the tensor type and data 
constructor. At some place in my code, in some definition (say, of a vector 
product), I want vectors and not more general tensors.

TP

On Saturday, April 27, 2013 16:16:49 Yury Sulsky wrote:

Hi TP,


Are you looking to use a phantom types here? Here's an example:


data One
data Two


data Tensor ndims a = Tensor { dims :: [Int], items :: [a] }
type Vector = Tensor One
type Matrix = Tensor Two


etc.



On Sat, Apr 27, 2013 at 3:33 PM, TP paratribulati...@free.fr wrote:

Hello,

I ask myself if there is a way to do the following.
Imagine that I have a dummy type:

data Tensor = TensorVar Int String

where the integer is the order, and the string is the name of the tensor.
I would like to make with the constructor TensorVar a type Vector, such
that, in pseudo-language:

data Vector = TensorVar 1 String

Because a vector is a tensor of order 1.

Is this possible? I have tried type synonyms and newtypes without any success.

Thanks a lot,

TP
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] partially applied data constructor and corresponding type

[TP]

Thanks for pointing to type level integers. With that I have found:

http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Types

For example:

---
data Zero = Zero
data Succ a = Succ a

class Card c where
c2num:: c - Integer

cpred::(Succ c) - c
cpred = undefined

instance Card Zero where 
c2num _ = 0

instance (Card c) = Card (Succ c) where
c2num x = 1 + c2num (cpred x)

main = do

putStrLn $ show $ c2num (Succ (Succ Zero))
---

I will continue to examine the topic in the following days, according to my 
needs.

Thanks a lot,

TP

On Sunday, April 28, 2013 07:58:58 Stephen Tetley wrote:
 What you probably want are type level integers (naturals)
 
 Yury Sulsky used them in the message above - basically you can't use
 literal numbers 1,2,3,... etc as they are values of type Int (or
 Integer, etc...) instead you have to use type level numbers:
 
 data One
 data Two
 
 Work is ongoing for type level numbers in GHC and there are user
 libraries on Hackage so there is a lot of work to crib from.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] partially applied data constructor and corresponding type

[TP]

Thanks a lot for your message.
I can use a recent version of GHC 7.6.x (I will install the last version of 
Kubuntu for that purpose).
However, it will take me some time to understand correctly this code (e.g. I 
do not know data kinds), I will go back to you if I encounter difficulties.

Thanks,

TP


On Monday, April 29, 2013 08:19:43 Richard Eisenberg wrote:
 There's a lot of recent work on GHC that might be helpful to you. Is it
 possible for your application to use GHC 7.6.x? If so, you could so
 something like this:
 
 {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
 
 data Nat = Zero | Succ Nat
 
 type One = Succ Zero
 type Two = Succ One
 type Three = Succ Two
 
 -- connects the type-level Nat with a term-level construct
 data SNat :: Nat - * where
   SZero :: SNat Zero
   SSucc :: SNat n - SNat (Succ n)
 
 zero = SZero
 one = SSucc zero
 two = SSucc one
 three = SSucc two
 
 data Tensor (n :: Nat) a = MkTensor { dims :: SNat n, items :: [a] }
 
 type Vector = Tensor One
 type Matrix = Tensor Two
 
 mkVector :: [a] - Vector a
 mkVector v = MkTensor { dims = one, items = v }
 
 vector_prod :: Num a = Vector a - Vector a
 vector_prod (MkTensor { items = v }) = ...
 
 specializable :: Tensor n a - Tensor n a
 specializable (MkTensor { dims = SSucc SZero, items = vec }) = ...
 specializable (MkTensor { dims = SSucc (SSucc SZero), items = mat }) = ...
 
 
 This is similar to other possible approaches with type-level numbers, but it
 makes more use of the newer features of GHC that assist with type-level
 computation. Unfortunately, there are no constructor synonyms or pattern
 synonyms in GHC, so you can't pattern match on MkVector or something
 similar in specializable. But, the pattern matches in specializable are
 GADT pattern-matches, and so GHC knows what the value of n, the type
 variable, is on the right-hand sides. This will allow you to write and use
 instances of Tensor defined only at certain numbers of dimensions.
 
 I hope this is helpful. Please write back if this technique is unclear!
 
 Richard


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] question about GADT and deriving automatically a Show instance

[TP]

Hi everybody,

I have a question about deriving automatically a Show instance when using 
GADT.
It works in this situation:


{-# LANGUAGE GADTs #-}

data Male
data Female

data Person gender where
Dead :: Person gender
Alive :: { name :: String
  , weight :: Float
  , father :: Person gender } - Person gender
 deriving Show

main = do

let a = Alive Joe 60 Dead :: Person Male
let b = Alive Jim 70 a :: Person Male

print a
print b


Indeed:

$ runghc test_show.hs 
Alive {name = Joe, weight = 60.0, father = Dead}
Alive {name = Jim, weight = 70.0, father = Alive {name = Joe, weight = 
60.0, father = Dead}}


But when I replace father :: Person gender by father :: Person gender2 
in the code (this is one of the advantages of GADT: with a classical 
algebraic data type declaration, gender2 would have to be a type variable 
for the data type), I obtain:

Can't make a derived instance of `Show (Person gender)':
  Constructor `Alive' must have a Haskell-98 type
  Possible fix: use a standalone deriving declaration instead
In the data declaration for `Person'

So I modify my code by removing deriving Show, and adding the line:

instance Show (Person gender)


But now, I obtain:

$ runghc test_show.hs 
GHC stack-space overflow: current limit is 536870912 bytes.
Use the `-Ksize' option to increase it.

Why (I imagine this is because there is an infinite loop in the construction 
of the show function)? Is there any workaround?

Thanks,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance

[TP]

Adam Gundry wrote:

[...]
 To use standalone deriving, you need to write
 
 deriving instance Show (Person gender)
 
 and everything will work fine. By writing
 
 instance Show (Person gender)
 
 you are instead giving an instance with no methods, and the default
 methods in the Show class contain a loop (so that one can define either
 show or showsPrec).

Thanks a lot. I did not remember that Standalone Deriving has a meaning as 
a GHC extension. My idea was correct, but the employed syntax was incorrect. 
Just for reference (future Google search by others), the corresponding link 
in the GHC documentation:

http://www.haskell.org/ghc/docs/7.6.2/html/users_guide/deriving.html

 P.S. You might like to check out the new DataKinds extension, which
 would allow Male and Female to be data constructors rather than type
 constructors.

Thanks a lot for pointing out this subject (it compells me to work on it - I 
am not an advanced user of GHC).
I have just tried to understand all this stuff about type and data 
constructor promotion:

http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/promotion.html

If I understand well, your idea is to avoid letting someone write:

let a = Alive Joe 60 Dead :: Person Int

which is nonsense (a Person cannot have a gender of type Integer), but 
legal code.
I have tried to use the technique described at the beginning of the article 
Given Haskell a Promotion, but I'm stuck. See the code below. My problem 
is that now Gender is a kind, no more a type, such that I cannot use it in 
the type definition of the GADT; but I am compelled to write something after 
::, and I cannot write for instance Dead :: Person Male because I want a 
dead person to be either a man or woman, of course. In fact, what I need is 
Gender both as a type and as a kind, if I am correct? What do I miss?

So the following version does not work:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}

data Gender = Male | Female

data Person :: Gender - * where
Dead :: Person Gender  -- WHAT DO I PUT HERE
Alive :: { name :: String
  , weight :: Float
  , father :: Person Gender } - Person Gender

deriving instance Show (Person Gender)

main = do

let a = Alive Joe 60 Dead :: Person Male
let b = Alive Jim 70 a :: Person Male

print a
print b


How to modify it?

Thanks a lot,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance

[TP]

Chris Wong wrote:

 data Person :: Gender - * where
 Dead :: Person Gender  -- WHAT DO I PUT HERE
 Alive :: { name :: String
   , weight :: Float
   , father :: Person Gender } - Person Gender
 
 Here's the problem. In the line:
 
 Dead :: Person Gender
 
 you are referring to the Gender *type*, not the Gender kind.
 
 To refer to the kind instead, change this to:
 
 Dead :: forall (a :: Gender). Person a
 
 This means for all types A which have the kind Gender, I can give you
 a Person with that type. The Alive declaration and deriving clause
 can be fixed in a similar way.
 
 Also, to enable the forall syntax, you need to add
 
 {-# LANGUAGE ExplicitForAll #-}
 
 at the top of the file.

Thanks a lot for your help. I did not realize the possible usage of a::b 
to indicate any type a of kind b. So I have adapted my code, and the 
following version is working correctly:


{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}

data Gender = Male | Female

data Person :: Gender - * where
Dead :: Person (a :: Gender)
Alive :: { name :: String
  , weight :: Float
  , father :: Person (a::Gender) } - Person (b :: Gender)

deriving instance Show (Person (a::Gender))

main = do

let a = Alive Joe 60 Dead :: Person Female
let b = Alive Jim 70 a :: Person Male


However, I have not managed to make the version with forall work. Below, the 
first occurrence of forall is ok, but the three following yield error.


{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ExplicitForAll #-}

data Gender = Male | Female

data Person :: Gender - * where
Dead :: forall (a :: Gender). Person a
Alive :: { name :: String
  , weight :: Float
  , father :: forall (a :: Gender). Person a } - forall (b :: 
Gender). Person b

deriving instance Show (forall (a :: Gender). Person a)

main = do

let a = Alive Joe 60 Dead :: Person Female
let b = Alive Jim 70 a :: Person Male


Thanks,

TP



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance

[TP]

Denis Kasak wrote:

 Note that all of this would work even without explicit quantification
 since you
 have already specified that Person accepts an argument of kind Gender. In
 other
 words, this works as expected:
 
 data Person :: Gender - * where
 Dead :: Person a
 Alive :: { name :: String
  , weight :: Float
  , father :: Person b } - Person a
 
 deriving instance Show (Person a)

Thanks so much, it is now perfectly clear. A lot of things learned with this 
dummy example.

TP




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] partially applied data constructor and corresponding type

[TP]

Richard Eisenberg wrote:

 There's a lot of recent work on GHC that might be helpful to you. Is it
 possible for your application to use GHC 7.6.x? If so, you could so
 something like this:
 
 {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
 
 data Nat = Zero | Succ Nat
 
 type One = Succ Zero
 type Two = Succ One
 type Three = Succ Two
 
 -- connects the type-level Nat with a term-level construct
 data SNat :: Nat - * where
   SZero :: SNat Zero
   SSucc :: SNat n - SNat (Succ n)
 
 zero = SZero
 one = SSucc zero
 two = SSucc one
 three = SSucc two
 
 data Tensor (n :: Nat) a = MkTensor { dims :: SNat n, items :: [a] }
 
 type Vector = Tensor One
 type Matrix = Tensor Two
 
 mkVector :: [a] - Vector a
 mkVector v = MkTensor { dims = one, items = v }
 
 vector_prod :: Num a = Vector a - Vector a
 vector_prod (MkTensor { items = v }) = ...
 
 specializable :: Tensor n a - Tensor n a
 specializable (MkTensor { dims = SSucc SZero, items = vec }) = ...
 specializable (MkTensor { dims = SSucc (SSucc SZero), items = mat }) = ...
 
 
 This is similar to other possible approaches with type-level numbers, but
 it makes more use of the newer features of GHC that assist with type-level
 computation. Unfortunately, there are no constructor synonyms or
 pattern synonyms in GHC, so you can't pattern match on MkVector or
 something similar in specializable. But, the pattern matches in
 specializable are GADT pattern-matches, and so GHC knows what the value of
 n, the type variable, is on the right-hand sides. This will allow you to
 write and use instances of Tensor defined only at certain numbers of
 dimensions.
 
 I hope this is helpful. Please write back if this technique is unclear!

Thanks a lot! Those days I have read about DataKinds extension (with help 
of Haskell-Cafe guys), and now I am able to understand your code. The 
technique to connect the type-level and term-level integers allows to 
duplicate information (duplicate information needed because of my more or 
less clear requirements in my previous posts), but in a safe way (i.e. with 
no copy/paste error): if I change one in two in the definition of the 
smart constructor mkVector, I obtain an error, as expected because of the 
use of type variable n on both sides of the equality in Tensor type 
definition (and then we understand why the type constructor SNat has been 
introduced).

This is a working example (this is not exactly what I will do at the end, 
but it is very instructive! One more time, thanks!):
--
{-# LANGUAGE DataKinds, GADTs, KindSignatures, StandaloneDeriving #-}

data Nat = Zero | Succ Nat

type One = Succ Zero
type Two = Succ One
type Three = Succ Two

-- connects the type-level Nat with a term-level construct
data SNat :: Nat - * where
SZero :: SNat Zero
SSucc :: SNat n - SNat (Succ n)

deriving instance Show (SNat a)

zero = SZero
one = SSucc zero
two = SSucc one
three = SSucc two

data Tensor (n :: Nat) a = MkTensor { order :: SNat n, items :: [a] }
deriving Show

type Vector = Tensor One
type Matrix = Tensor Two

mkVector :: [a] - Vector a
mkVector v = MkTensor { order = one, items = v }

-- some dummy operation defined between two Vectors (and not other order
-- tensors), which results in a Vector.
some_operation :: Num a = Vector a - Vector a - Vector a
some_operation (MkTensor { items = v1 }) (MkTensor { items = v2 }) =
mkVector (v1 ++ v2)

main = do

let va = mkVector ([1,2,3] :: [Integer])
let vb = mkVector ([4,5,6] :: [Integer])

print $ some_operation va vb
print $ order va
print $ order vb
-


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] accessing a type variable in instance declaration

[TP]

Hi all,

I wonder if there is some means to get a type variable value in the body of 
a class instance definition. It seems it is not possible (a workaround has 
already been given on this list), but I would like a confirmation.
For example, imagine that I have a Tensor type constructor, that takes a 
type-level integer (representing the Tensor order) to make a concrete type:

-
instance Show (Tensor order) where
 show TensorVar str = show tensor  ++ str ++  of order 
++ (show (c2num order))
--

where c2num transforms a type-level integer to an integer, through 
typeclasses (see 
http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Types)

I obtain a compilation error: order is not known in the body of the 
instance. Putting ScopedTypeVariable as extension does not change anything 
(http://www.haskell.org/ghc/docs/7.0-latest/html/users_guide/other-type-extensions.html#scoped-type-variables).

I have tried also using forall, without more success:


instance forall order. Show (Tensor order) where
  show TensorVar str = show ”tensor ” ++ str ++ ” of order ”
++ (show (c2num order))


Thanks in advance,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] accessing a type variable in instance declaration

[TP]

Roman Cheplyaka wrote:

 You are confusing type and value variables.
 
   c2num order
 
 means apply the function 'c2num' to the value variable 'order', which is
 not defined.
 
 To get from a type to a value you can use a type class 'Sing' (for
 'singleton')
 
   class Sing a where
 sing :: a
 
   instance Sing Zero where
 sing = Zero
 
   instance Sing a = Sing (Succ a) where
 sing = Succ sing
 
 After adding the appropriate constraint to the instance, you can write
   
   show $ c2num $ (sing :: order)

Ok, thanks, I understand. Now, I'm stuck to compile this code (independent 
from my previous post, but related to it):

---
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data Nat = Zero | Succ Nat
type One = Succ Zero
type Two = Succ One

-- class Cardinal c where   -- line 1
class Cardinal (c::Nat) where  -- line 2
c2num :: c - Integer
cpred :: (Succ c) - c
cpred = undefined

instance Cardinal Zero where
c2num _ = 0

instance (Cardinal c) = Cardinal (Succ c) where
c2num x = 1 + c2num (cpred x)

main = do

print $ show $ c2num (undefined::Succ (Succ Zero))
print $ show $ c2num (undefined::Two)
-

With line 2, I get:

test_nat.hs:11:14:
Kind mis-match
Expected kind `OpenKind', but `c' has kind `Nat'
In the type `c - Integer'
In the class declaration for `Cardinal'

With line 1 instead, I get:

Kind mis-match
The first argument of `Succ' should have kind `Nat',
but `c' has kind `*'
In the type `(Succ c) - c'
In the class declaration for `Cardinal'

So, in the first case, c has a too restricted kind, and in the second one, 
it has a too broad kind in the definition of cpred. I have tried several 
things without any success.
How to compile that code?

Thanks,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] question about type constructors

[TP]

Hi,

In the program I am trying to write, I have a problem that can be reduced to 
the following dummy example:

--
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}

class PrettyPrint a where
prettify :: a - String

data Gender = Male | Female | Gender3 | Gender4

data Person :: Gender - * where
Person :: String - Person b
Child :: String - Person a - Person b - Person c

instance PrettyPrint (Person a)

instance PrettyPrint (Person Male) where
prettify (Person name) = My name is  ++ (show name)
  ++  and I am a male
prettify (Child name person1 person2) = My name is  ++ (show name)
  ++  and my parents are: ++ (prettify person1) ++ , 
  ++ (prettify person2)

main = do

let p1 = Person Jim :: Person Male
let p2 = Person Joe :: Person Male
let p3 = Child Jack p1 p2

print $ prettify p1
print $ prettify p2
print $ prettify p3
--

The idea is that I want to implement PrettyPrint only for a subset of the 
possible types in Gender (through promotion process). Why? It would be 
longer to explain (it is a bit more complicated in my real program).

Anyway, in the program above, I have found that with IncoherentInstances 
(and the empty instance definition for (Person a)), it is working, it is 
able to use the most specific instance corresponding to the current type (I 
don't know exactly why). For example, p1 and p2 are correctly printed above, 
because they are of type (Person Male) and because I have implemented 
PrettyPrint for (Person Male).

But it does not work for p3, I obtain an error at runtime:
-
$ runghc test.hs
My name is \Jim\ and I am a male
My name is \Joe\ and I am a male
test_typelost.hs: test_typelost.hs:16:10-31: No instance nor default method 
for class operation Main.prettify
-

The reason is that the information that p1 and p2 are Male seems to be 
lost when we construct the child Child Jack p1 p2, probably because 
GHC only sees that in the type signature of Child, we have a more general 
(Person a) - (Person b). So he tries to find an implementation of prettify 
in PrettyPrint (Person a), but there is none.

Is there any workaround?

Thanks,

TP



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] question about type constructors

[TP]

Roman Cheplyaka wrote:

 The rule of thumb is that you should never use IncoherentInstances.
 
 The proper way to do it is:
 
   data Person :: Gender - * where
   Person :: String - Person b
   Child
 :: (PrettyPrint a, PrettyPrint b)
 = String - Person a - Person b - Person c

Thanks a lot. Now I am using FlexibleContexts, and it works correctly (see 
code below). I think I have understood the problem.
However, I have still one question. In the code below, I have added data 
constructors Child2, Child3 (imagining a world where every people has 
three children). The problem is that I am compelled to repeat the context 
(PrettyPrint (Person a), PrettyPrint (Person b)) for each one of the 
constructors. Is there any way to specify the context only once? I have 
tried using forall, but without any success.

Thanks,

TP

-
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

class PrettyPrint a where
prettify :: a - String

data Gender = Male | Female | Gender3 | Gender4

data Person :: Gender - * where
Person :: String - Person b
Child1 :: (PrettyPrint (Person a)
 , PrettyPrint (Person b)
 ) = String - Person a - Person b - Person c
Child2 :: (PrettyPrint (Person a)
 , PrettyPrint (Person b)
 ) = String - Person a - Person b - Person c
Child3 :: (PrettyPrint (Person a)
 , PrettyPrint (Person b)
 ) = String - Person a - Person b - Person c

instance PrettyPrint (Person Male) where
prettify (Person name) = My name is  ++ (show name)
  ++  and I am a male
prettify (Child1 name person1 person2) = My name is  ++ (show name)
  ++  and my parents are: ++ (prettify person1) ++ , 
  ++ (prettify person2)

main = do

let a = Person Jim :: Person Male
let b = Person Joe :: Person Male
let c = Child1 Jack a b :: Person Male

print $ prettify a
print $ prettify b
print $ prettify c


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] GADT and instance deriving

[TP]

Hello,

I continue my learning of not so obvious Haskell/GHC topics when 
encountering problems in the code I write.
Below is a small example of an heterogeneous list, using GADT, inspired 
from:
http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types#Example:_heterogeneous_lists

--
{-# LANGUAGE GADTs #-}

data Box where
Box :: Eq s = s - Box

instance Eq Box where

(Box s1) == (Box s2) = s1 == s2
--

This code does not compile, because GHC is not sure that s1 and s2 have the 
same type:

--
Could not deduce (s ~ s1)
from the context (Eq s)
  bound by a pattern with constructor
 Box :: forall s. Eq s = s - Box,
   in an equation for `=='
  at test_eq_GADT_before.hs:8:6-11
[and more lines...]
--

(Do you confirm that tilde in s~s1 means s has the same type as s1? I have 
not found this information explicitly in the Haskell stuff I have read).

I have googled on the topic, and found:
http://stackoverflow.com/questions/6028424/defining-eq-instance-for-haskell-gadts
From the proposed solution, I wrote:

--
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}

import Data.Typeable

data Box where
Box :: (Typeable s, Eq s) = s - Box
deriving Typeable

instance Eq Box where

(Box s1) == (Box s2) = Just s1 == cast s2
--

that seems to work correctly:
--
let a = Box (2::Int)
let b = Box (2::Float)

print $ a == b
print $ a == a
--

Is this the right way to go? Is there any other solution?

Thanks,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] GADT and instance deriving

[TP]

Alexander Solla wrote:

 (Do you confirm that tilde in s~s1 means s has the same type as s1? I
 have
 not found this information explicitly in the Haskell stuff I have read).

 
 Yes.
 
 http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/equality-constraints.html
 
 Is this (Typeable) the right way to go? Is there any other solution?

 
 Using typeable is a perfectly reasonable way to go.

Thanks for your help.
Unfortunately, I am in the following case (in my real code, not the dummy 
example of my initial post):

http://haskell.1045720.n5.nabble.com/Can-t-make-a-derived-instance-of-Typeable-A-B-A-has-arguments-of-kind-other-than-td3121994.html

Indeed, I obtain at compilation:

Can't make a derived instance of `Typeable (Tensor ($a))':
  `Tensor' must only have arguments of kind `*'

Tensor is a type constructor which takes a type-level integer as argument 
to make a concrete type Tensor order (so its kind is Nat - *).
Thus in my real code, I cannot derive the typeable instance automatically. I 
am compelled to write an instance of typeable for my GADT. Are there some 
tutorial around here? Because the documentation page is a bit terse for my 
level of knowledge:

http://www.haskell.org/ghc/docs/latest/html/libraries/base/Data-Typeable.html

In the first link above, someone writes:


You'll have to manually
write a Typeable instance if you want one.  The process is somewhat
trickier than you might expect, due to the fact that Typeable does
some unsafe stuff.  But there are plenty of examples for how to do it
safely. 


Where are these examples that can help me to write my instance?
I have tried to read the source of the implemented instances in 
data.typeable, not so easy for me.

Thanks,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] GADT and instance deriving

[TP]

TP wrote:

 Where are these examples that can help me to write my instance?
 I have tried to read the source of the implemented instances in
 data.typeable, not so easy for me.

Ok, by doing a better search on Google (instance typeable  blog), I have 
found interesting information:

http://blog-mno2.csie.org/blog/2011/12/24/what-are-data-dot-typeable-and-data-dot-dynamic-in-haskell/

and especially:

http://hauptwerk.blogspot.fr/2012/11/coming-soon-in-ghc-head-poly-kinded.html


In this new class, we are no longer restricted to datatypes with a maximum 
of 7 parameters, nor do we require the parameters to be of kind *.


So, I have to try that.
I will give some feedback here (from my beginner point of view).

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] GADT and instance deriving

[TP]

Hi Richard,

Thanks a lot for your answer.
We had a discussion about some Tensor type some time ago:

https://groups.google.com/d/msg/haskell-cafe/Rh65kdPkX70/T2zZpV6ZpjoJ

Today I have a type constructor Tensor in which there is a data 
constructor Tensor (among others):


data Tensor :: Nat - * where
[...]
Tensor :: String - [IndependentVar] - Tensor order
[...]


The idea is that, for example, I may have a vector function of time and 
position, for example the electric field:

E( r, t )

(E: electric field, r: position vector, t: time)

So, I have a Tensor (E) that depends on two tensors (r and t). I want to put 
r and t in a list, the list of independent variable of which E is a 
function. But we see immediately that r and t have not the same type: the 
first is of type Tensor One, the second of type Tensor Zero. Thus we 
cannot put them in a list. This is why I have tried to use an heterogeneous 
list:

http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types#Example:_heterogeneous_lists

Thus in the first place the problem comes from the fact that I have put the 
order of the Tensor in the type rather than in the data constructors. But it 
is useful:

* I can make type synonyms
type Scalar = Tensor Zero
type Vector = Tensor One
[...]

* with multi-parameter typeclasses, I can define operations as:

class Division a b c | a b - c where
 (/) :: a - b - c

and then I implement these operations on a subset of types:

instance (PrettyPrint (Tensor a)) = Division (Tensor a) Scalar (Tensor a) 
where
   ZeroTensor / _ = ZeroTensor
   _ / ZeroTensor = error Division by zero!
   t / s = Divide t s

So, the code is clear, and instead of runtime dimension checks, everything 
is detected at compilation. So the choice of putting the order in the type 
seems to be correct.
My only need to use Typeable comes from the heterogeneous list. But how to 
do without?

Thanks,

TP



Richard Eisenberg wrote:

 Thankfully, the problem you have is fixed in HEAD -- the most recent
 version of GHC that we are actively working on. I am able, using the HEAD
 build of GHC, to use a `deriving Typeable` annotation to get a Typeable
 instance for a type that has non-*-kinded parameters. To get the HEAD
 compiler working, see here:
 http://hackage.haskell.org/trac/ghc/wiki/Building
 
 However, I'm worried that other aspects of your design may be suboptimal.
 The `Box` type you mentioned a few posts ago is called an existential
 type. Existential types have constructors who have type parameters that
 are *not* mentioned in the conclusion. As an example, your `Box`
 constructor involved a type parameter `a`, but the `Box` type itself has
 no parameters. This existential nature of the type is why your comparison
 didn't work.
 
 A Tensor, however, doesn't seem like it would need to be an existential
 type. The order of the tensor should probably (to my thinking) appear in
 the type, making it not existential anymore.
 
 In general, I (personally -- others will differ here) don't love using
 Typeable. By using Typeable, you are essentially making a part of your
 program dynamically typed (i.e., checked at runtime). The beauty of
 Haskell (well, one of its beauties) is how it can check your code
 thoroughly at compile time using its rich type language. This prevents the
 possibility of certain bugs at runtime. Using Typeable circumvents some of
 that, so I would recommend thinking carefully about your design to see if
 its use can be avoided.
 
 Just to diffuse any flames I get for the above paragraph: I fully support
 the role of Typeable within Haskell. Indeed, sometimes it is unavoidable.
 In fact, I have a small update to the Typeable interface on my to-do list
 (adding functionality, not changing existing). I am just arguing that its
 use should be judicious.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] GADT and instance deriving

[TP]

Hi Tillmann and Richard,

Thanks for your answers.

I have tried to analyze the code snippets you proposed.
I've tried to transpose your examples to what I need, but it is not easy.

The problem I see with putting the list of independent variables (*) at the 
type level is that at some time in my code I want for instance to perform 
formal mathematical operations, for example I want a function deriv that 
takes f(x(t),y(t),z(t)) as input, and returns

df/dt = ∂f/∂x*dx/dt + ∂f/∂y*dy/dt + ∂f/∂z*dz/dt

If the list of dependencies is encoded at the type level, I don't see how to 
produce the previous output from the knowledge of f(x(t),y(t),z(t)). You 
understand that what I want to do is some type of basic Computer Algebra 
System library.

Moreover, I want overloading for infix functions as '*', '/', '⋅' (scalar 
product), × (vector product) etc., that is why I have used typeclasses (see 
the code I showed in my previous post). For example, for the time being I 
will restrict myself to scalar product between vector and vector, vector and 
dyadic, dyadic and vector (a dyadic is a tensor of order 2, a matrix if you 
prefer). So I have three instances for scalar product '⋅'. I don't see how 
to combine this idea of overloading or derivation function with what you 
proposed. But I have perhaps missed something.

Thanks,

TP

(*): That is to say the list of tensors of which one tensor depends, e.g. 
[t,r] for E(t,r), or simply [x,y,z] for f(x(t),y(t),z(t)) where x, y, and z 
themselves are scalars depending on a scalar t). In the test file of my 
library, my code currently looks like:

-
type Scalar = Tensor Zero
type Vector = Tensor One
[...]
let s = (t s []) :: Scalar
let v = (t v [i s]) :: Vector
let c1 = v + v
let c2 = s + v⋅v
-

t is a smart constructor taking a string str and a list of independent 
variables, and makes a (Tensor order) of name str.

So in the example above, s is a scalar that depends on nothing (thus it is 
an independent variable), v is a vector that depends on s (i is a smart 
constructor that wraps s into a Box constructor, such that I can put all 
independent variables in an heterogeneous list).
c1 is the sum of v and v, i.e. is equal to 2*v.
c2 is the sum of s and v scalar v.
If I try to write:

let c3 = s + v

I will obtain a compilation error, because adding a scalar and a vector has 
no meaning.

Is there some way to avoid typeable in my case?

Moreover, if I wanted to avoid the String in the first argument of my smart 
constructor t, such that

let s = (t []) :: Scalar

constructs an independent Scalar of name s, googling on the topic seems to 
indicated that I am compelled to use Template Haskell (I don't know it at 
all, and this is not my priority).
Thus, in a general way, it seems to me that I am compelled to use some 
meta features as typeable or Template Haskell to obtain exactly the result 
I need while taking benefit from a maximum amount of static type checking.


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] question about singletons

[TP]

Hi all,


Following a discussion on Haskell Cafe some time ago (1), Roman C. wrote:


On the other hand, the type 'Succ 'Zero has kind 'Nat and doesn't have
any inhabitants — only types of kind * do.


Indeed, this is what seems to occur in the following example:

---
{-# LANGUAGE DataKinds #-}

data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )

main = do

let one = undefined :: 'Succ 'Zero
print one
---

We obtain an error (ghc 7.6.2):
---
Kind mis-match
Expected kind `OpenKind', but `Succ Zero' has kind `Nat'
In an expression type signature: Succ Zero
In the expression: undefined :: Succ Zero
In an equation for `one': one = undefined :: Succ Zero
---

(note that the error is slightly different in the HEAD version of GHC (2)).
Is it related to the sentence As bottom is an inhabitant of every type 
(though with some caveats concerning types of unboxed kind), bottoms can be 
used wherever a value of that type would be.  found at address (3)? Here we 
have a non-* kind, such that bottom would not be an inhabitant of ('Succ 
'Zero). Why is this so? This seems to be an assumed choice (4), but I would 
like to understand the reason for this design, which makes necessary to use 
singletons, as explained at (4).

Now, if I use a singleton to make my example work, I obtain an error when 
trying to make the type (Sing a) an instance of Show:

---
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )

data Sing :: a - *

deriving instance Show (Sing a)

main = do

let one = undefined :: Sing ('Succ 'Zero)
print one
---

The error is simply:

---
test_noinhabitant_corrected.hs: Void showsPrec
---

Why?

Thanks,

TP


References:
--

(1):
https://groups.google.com/forum/?fromgroups#!topic/haskell-cafe/AltmX5iCFi8

(2):
---
Expected a type, but ‛Succ Zero’ has kind ‛Nat’
In an expression type signature: Succ Zero
In the expression: undefined :: Succ Zero
In an equation for ‛one’: one = undefined :: Succ Zero
---

(3):
http://www.haskell.org/haskellwiki/Bottom

(4):
http://hackage.haskell.org/trac/ghc/wiki/TypeNats/Basics


Both numeric and symbol literal types are empty---they have no inhabitants. 
However, they may be used as parameters to other type constructors, which 
makes them useful. 



A singleton type is simply a type that has only one interesting inhabitant.




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] question about singletons

[TP]

Thanks Richard for your detailed answer.
Please find my reply below (note I have rearranged some of your paragraphs).

Richard Eisenberg wrote:

 * Types at kind other than * do not have any inhabitants -- in fact, some
 people would hesitate to call type-like things at kind other than * types!
 (Though, I will call these things types because there's just not another
 good moniker. Type-level data? Type indices? Type constructors? All are
 somehow lacking.) Let's start with a more familiar example: Maybe. To form
 an inhabited type, we must apply Maybe to something. So, we can have
 values of type (Maybe Int) and values of type (Maybe Bool), but not values
 of plain old type (Maybe). That's because Maybe has kind (* - *), not
 kind *. Another way to say this is what I said above: Maybe requires
 something (something at kind *, specifically) to become a proper,
 inhabited type. And, even though we say `undefined` exists at all types,
 that's a bit of a simplification. `undefined` exists at all types _of kind
 *_. The full type of `undefined` is `forall (a :: *). a`. Thus, we can't
 have `undefined` at Maybe, because Maybe is not of kind *.
[...]
 (When I first wandered down this road, I was confused by this too. Part of
 the confusion was somehow deciding that * had some vague association with
 * as used on the command line -- a notation that could expand to something
 else. This is totally, completely, and in every way False. In at least one
 other programming language [Coq], what Haskell spells * is spelled `Type`.
 [Well, almost.])
[...]
 Why have the restriction that kinds other than * are uninhabited? Well,
 for one, (-) would be a strange beast indeed if other types could be
 inhabited. What would be the kind of (-)? I don't want to think about it.

In other words, bottom can be an inhabitant of a concrete type, not a type 
constructor, which I can understand. But a type of kind Nat is a concrete 
type, so why bottom cannot be an inhabitant of this type?

 We also have the nice maxim that every type that appears to the right of a
 :: must be of kind *.

This is a rule set into Haskell, but why not a type of kind Nat, which is a 
concrete type?

 This argument extends directly to where we have types derived from
 promoted data constructors. The type 'Zero has kind Nat, not *, so 'Zero
 is uninhabitable, even by `undefined`.

I can understand that if indeed the definition of undefined is `forall (a :: 
*). a` (see above), undefined is not suitable to represent ”bottom” for a 
type of kind Nat. But I don't see why there cannot be a bottom in a type of 
kind Nat; isn't it more a limitation related to the Haskell definition of 
undefined that prevents undefined to be used to mean bottom in Haskell 
for a type of kind different from `*`?

 data Proxy a = P
[...]
 data SNat :: Nat - * where
   SZero :: SNat 'Zero
   SSucc :: SNat n - SNat ('Succ n)
 
 Now, you can have values that are tightly associated with types. Yay!

Thanks for these definitions, which I have recorded in my notes.

 * Why did you get that error with `show`? Because the `Sing` type you
 defined is uninhabited -- not because it has a funny kind, but because it
 has no constructors. So, when a `Show` instance is derived, the `show`
 method just fails -- GHC knows `show` at type `Sing` cannot be called
 because there are no `Sing`s. Then, when you subvert this logic by using
 `undefined`, the derived `show` method doesn't quite know what to do with
 itself.

I think I understand what you say, but I am not sure to understand the 
reason. For example, consider the trivial examples in part (1) of Post 
Scriptum below. We have a concrete type Foo clearly of kind `*`, so bottom 
(undefined in Haskell) is an inhabitant of Foo. Why should I be compelled to 
add another inhabitant (a data constructor) to get bottom printed? Bottom 
existence is independent from other inhabitants, isn't it?

 I hope this helps! I do have to say I'm impressed, TP, by your intrepid
 path of discovery down this road. You're asking all the right questions!

Thanks Richard. I am discovering things in Haskell every day. In the last 
weeks, I have especially been amazed by all the extensions in GHC compared 
to Haskell 2010 standard. In fact, there are two things: Haskell, and GHC (I 
don't know Hugs at all). A textbook on GHC is perhaps missing, using 
advanced extensions and comparing with pure Haskell.

I did not follow type or category theory lectures at all, I am an electrical 
engineer in France interested in Physics during my leasure time. To make 
some complicated calculations, I need a Computer Algebra System with certain 
features that does not exist yet. Rather than adapting an existing CAS to my 
needs (Maxima, Axiom, Sympy, etc.), I thought that it was a good occasion to 
learn a language as OCaml or Haskell (and so to code in a clearer way than 
in Python for serious programs, through strong typing). I began with 
OCaml, but switched rapidly to Haskell

Re: [Haskell-cafe] question about singletons

[TP]

Thanks Richard, now I have my answers.

Richard Eisenberg wrote:

 - The type system of Haskell is based on theoretical work that resolutely
 assumes that types of non-* kind are uninhabited. While it is possible to
 stretch imagination to allow types like 'Zero to be inhabited, the
 designers of Haskell would have a lot of work to do to prove that the new
 language is actually type-safe.
[...]
 Technically, yes, we could have a
 different definition of undefined, but it would fly in the face of a lot
 of theory about type-safe programming languages. This is not to say that
 such a thing is impossible, but just perhaps imprudent.

Ok, this is a convincing reason to admit that non-* kinded types must be 
uninhabited, even by undefined.

 Bottom is inherently uninteresting, because you never see bottom in
 running code, and you can never know where bottom is lurking (other than
 after your program has crashed).
[...]
 So, all of this is to say that undefined is entirely uninteresting, as
 your program can never know when it encounters one without dying.

Ok: Haskell refuses to show undefined for a type of kind * if it has not 
another inhabitant, because the type is deemed uninteresting.

 Technically, bottom should have this
 definition (which is perfectly valid Haskell):
 
 bottom :: a
 bottom = bottom
 
 In other words, bottom is infinite recursion -- a term that never finishes
 evaluating. Let's say a show method tried to print its argument and its
 argument is bottom. Well, that method would have to examine its argument
 and would immediately fall into an infinite loop. Bottom is a little like
 Medusa when you have no mirrors around. Once you look at it, it's too
 late.
 
 In Haskell, we don't usually use bottom in this way; we use undefined.
 undefined masquerades as bottom, but instead of forcing a running program
 into an infinite loop, looking at undefined causes a running program to
 instantly terminate. This is generally much nicer than an infinite loop,
 but this niceness is simply a convenience that the compiler gives us. From
 a theoretical point of view, a hung program is much cleaner. To recover
 the consistency of the theory, Haskell provides no way to recover from a
 discovery of undefined in a running program. (GHC has implemented an
 exception that allows exception-handling code, written in the IO monad, to
 catch a use of undefined, but I would be highly suspicious of code that
 used this feature.)

Interesting, I will remember that.

Thanks

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Typeable typeclass and type-level naturals

[TP]

Hi all,

I try to play with the Typeable typeclass, and I have some difficulties to 
make it work in this simple case where I use type-level naturals:

-
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

import Data.Typeable

data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord, Typeable )

data Box where
Box :: (Typeable s, Show s, Eq s) = s - Box
deriving Typeable

data Proxy a = P deriving Typeable

deriving instance Show Box
instance Eq Box where

(Box s1) == (Box s2) = Just s1 == cast s2

main = do

let one = undefined :: Main.Proxy ('Succ 'Zero)
let foo = Box one
print foo
-

I obtain:

-
No instance for (Typeable Nat 'Zero) arising from a use of ‛Box’
In the expression: Box one
In an equation for ‛foo’: foo = Box one
In the expression:
  do { let one = ...;
   let foo = Box one;
   print foo }
-

Note that it is necessary to use the HEAD version of GHC to obtain this 
message (I use version 7.7.20130525); with GHC 7.6.2, the message is 
different because recent improvements in Typeable are not present (1).

What is the problem? I've tried different things without success.
Tell me if the beginners diffusion list is more suitable than Haskell-
Cafe.

Thanks,

TP


(1): 
http://hauptwerk.blogspot.fr/2012/11/coming-soon-in-ghc-head-poly-kinded.html


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Typeable typeclass and type-level naturals

[TP]

Roman Cheplyaka wrote:

 Try adding
 
   deriving instance Typeable 'Zero
   deriving instance Typeable a = Typeable ('Succ a)
 
 to your module.
 
 (I haven't tested it — you might need to tweak it a bit.)

Thanks Roman.
Unfortunately, I already tried that (without the constraint Typeable a =, 
what a fool), but it did not work. The error is the same with the 
constraint:

Derived typeable instance must be of form (Typeable 'Succ)
In the stand-alone deriving instance for
  ‛Typeable a = Typeable (Succ a)’

What is the problem?

Is it possible that it is a bug in GHC? Indeed, we had unwanted similar 
error messages recently:

http://hackage.haskell.org/trac/ghc/ticket/7704

Thanks,

TP

PS: the complete program for a test that shows the error:
--
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

import Data.Typeable

data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord, Typeable )

deriving instance Typeable 'Zero
deriving instance Typeable a = Typeable ('Succ a)

data Box where
Box :: (Typeable s, Show s, Eq s) = s - Box
deriving Typeable

data Proxy a = P deriving Typeable

deriving instance Show Box
instance Eq Box where

(Box s1) == (Box s2) = Just s1 == cast s2

main = do

let one = undefined :: Main.Proxy ('Succ 'Zero)
let foo = Box one
print foo


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Typeable typeclass and type-level naturals

[TP]

José Pedro Magalhães wrote:

 Oh, it should probably be simply

   deriving instance Typeable 'Zero
   deriving instance Typeable 'Succ

 
 Yes, that's how it should be. Please let me know if that
 doesn't work.

Thanks, it works perfectly like that.
I don't understand exactly why the previous syntax did not work, but maybe 
it will be clearer when I finish the paper Scrap your boilerplate: a 
practical design pattern for generic programming (anyway, this paper seems 
very interesting).
Output of the code:

-
$ runghc-head test_typeable.hs 
Box test_typeable.hs: Prelude.undefined
-

Maybe the Box  in front of the line is strange, but it is OK: one is 
undefined, not Box one.

This is the full tested code, for sake of reference:

---
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

import Data.Typeable

data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )

deriving instance Typeable 'Zero
deriving instance Typeable 'Succ

data Box where
Box :: (Typeable s, Show s, Eq s) = s - Box
deriving Typeable

data Proxy a = P deriving (Typeable, Show, Eq)

deriving instance Show Box
instance Eq Box where

(Box s1) == (Box s2) = Just s1 == cast s2

main = do

let one = undefined :: Main.Proxy ('Succ 'Zero)
let foo = Box one
print foo
--

Thanks a lot,

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

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

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

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

[TP]

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] putting the result of a function in `infix` declaration

[TP]

Hi everyone,

Consider the following code:

--
import Prelude hiding ((+))

data Expr = Plus Expr Expr | Minus Expr Expr | Expr String deriving Show

f :: Expr - Int
f (Plus _ _) = 1
f (Minus _ _) = 2

-- infix (f (Plus undefined undefined)) +  -- (*)
infix 6 +
(+) :: Expr - Expr - Expr
e1 + e2 = Plus e1 e2

main = do

let a = Expr a
let b = Expr b
print $ a + b
--

I would like to declare the infix precedence of (+) with a function 
(commented line (*)) instead of directly as above.

Is there any means to do that?
Do we need some kind of preprocessing machinery? How to do that in Haskell?

In a more general way, let us suppose I have a Haskell library able to 
perform some calculations: how to use it in a pre-processing step, before 
compilation of the executable? It could be a function to compute 
symbolically roots of a polynomial of second degree to be used at runtime. 
We would put some placeholders in the code where the result of the pre-
processing calculation would enter.

Thanks in advance,

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

[TP]

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

[Haskell-cafe] some questions about Template Haskell

[TP]

Hi everybody,

I am trying to learn Template Haskell, and I have two independent questions.

1/ First, the following code (which is not in its final version, but it is a 
test) does not compile:

---
{-# LANGUAGE TemplateHaskell #-}
module Pr where
import Language.Haskell.TH

pr :: Name - ExpQ
pr n = [| putStrLn $ (nameBase n) ++  =  ++ show $(varE n) |]
---

I obtain:

---
No instance for (Lift Name) arising from a use of `n'
Possible fix: add an instance declaration for (Lift Name)
In the first argument of `nameBase', namely `n'
---

Why? Indeed, there is no typeclass constraint on n in the definition of 
nameBase:

ghci :t nameBase
nameBase :: Name - String

Contrary to lift for example:
ghci :t lift
lift :: Lift t = t - Q Exp

2/ If I define in a module:

j = 3

and then define in another module:

---
h x = $([|j|])
main = do
print $ h undefined
---

I obtain 3 as expected.

However, I do not achieve to make this system work with an infix 
declaration:

infix $([| j |]) +

I obtain:

parse error on input `$('

What is the problem?


Thanks in advance,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] some questions about Template Haskell

[TP]

TP wrote:

 2/ If I define in a module:
 
 j = 3
 
 and then define in another module:
 
 ---
 h x = $([|j|])
 main = do
 print $ h undefined
 ---
 
 I obtain 3 as expected.
 
 However, I do not achieve to make this system work with an infix
 declaration:
 
 infix $([| j |]) +
 
 I obtain:
 
 parse error on input `$('

I don't know what happens exactly, but one way to get out of this problem is 
to write the complete top-level declaration with a splice, instead of only 
the fixity level:

$(return $ [ InfixD (Fixity $([| j |]) InfixN) (mkName +) ])

Concerning my first question, I have not been able to understand what 
happens at this time. I continue to look at it.

Thanks,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] some questions about Template Haskell

[TP]

o...@okmij.org wrote:

 pr :: Name - ExpQ
 pr n = [| putStrLn $ (nameBase n) ++  =  ++ show $(varE n) |]
 
 The example is indeed problematic. Let's consider a simpler one:
 
 foo :: Int - ExpQ
 foo n = [|n + 1|]
 
 The function f, when applied to an Int (some bit pattern in a machine
 register), produces _code_. It helps to think of the code
 as a text string with the
 source code. That text string cannot include the binary value that is
 n. That binary value has to be converted to the numeric text string, and
 inserted in the code. That conversion is called `lifting' (or
 quoting). The function foo is accepted because Int is a liftable type,
 the instance of Lift. And Name isn't.

Thanks Oleg,
Probably the following question will be stupid, but I ask it anyway: in my 
initial example, (nameBase n) returns a String, so we are not in the case 
where it is not liftable? In fact I am not sure to have understood your 
answer.

Now, I have found another behavior difficult to understand for me:

 runQ $ lift u
ListE [LitE (CharL 'u')
 runQ $ [| u |]
LitE (StringL u)

So we have similar behaviors for lift and [||]. We can check it in a splice:

 $( [| u |] )
u
 $( lift u )
u

But if I replace a working version:

pr n = [| putStrLn ( $(lift( nameBase n ++  =  )) ++ show $(varE n) ) |]

by

pr n = [| putStrLn ( $([| (nameBase n) ++  =  |]) ++ show $(varE n) ) |]

I again get the error 


No instance for (Lift Name) arising from a use of `n'
Possible fix: add an instance declaration for (Lift Name)
In the first argument of `nameBase', namely `n'


It is not easy to surmise the reason for this error.

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] some questions about Template Haskell

[TP]

John Lato wrote:

 The problem isn't the output of nameBase, it's the input parameter 'n'. 
 In your example, you've created a function that takes input (a Name) and
 generates code based upon that input.  In order to lift a value (n) from
 an ordinary context into a quote, it needs a Lift instance.

Thanks John.
Ok I can understand that a Lift instance is needed, but to use the lift 
function below, we also need a Lift instance for the return of (nameBase n), 
because lift is a function that operates on instances of the Lift typeclass:

 :i lift
class Lift t where
  lift :: t - Q Exp

And it is indeed the case:
 :i Lift
[...]
instance Lift a = Lift [a]
instance Lift Char

And as I have shown on a small example, lift and [||] return about the same 
result:

 runQ $ lift u
ListE [LitE (CharL 'u')
 runQ $ [| u |]
LitE (StringL u)

So what is the difference between lift and [||]?
Although I feel stupid, I cannot lie and claim I have understood.

 Perhaps it helps if you think about what a quote does: it allows you to
 write essentially a string of Haskell code that is converted into an AST.
  For this to work, the quote parser needs to know how to generate the AST
 for an identifier.  Like much of Haskell, it's type-driven.  For
 identifiers in scope from imports, TH simply generates a variable with the
 correct name.  But for data, the parser needs a way to generate an AST
 representation, which is what Lift is for.

Ok, I think I understand that (we need some method to transform a value at 
data level in a token of an AST), but it seems to me it does not answer my 
question above. But I am probably wrong.

Thanks

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] some questions about Template Haskell

[TP]

John Lato wrote:

 Now, I have found another behavior difficult to understand for me:

  runQ $ lift u
 ListE [LitE (CharL 'u')
  runQ $ [| u |]
 LitE (StringL u)

 So we have similar behaviors for lift and [||]. We can check it in a
 splice:

  $( [| u |] )
 u
  $( lift u )
 u

 But if I replace a working version:

 pr n = [| putStrLn ( $(lift( nameBase n ++  =  )) ++ show $(varE n) )
 |]   - case (i) -

 by

 pr n = [| putStrLn ( $([| (nameBase n) ++  =  |]) ++ show $(varE n) )
 |]   - case (ii) -

 I again get the error

 
 In the working version, 'n' appears inside a splice, whereas in the other
 n
 is in a quote.  AFAIK any value can be used in a splice (provided it meets
 the staging restrictions), whereas only Lift-able values can be used in a
 quote.

If I take this as a granted axiom, then I can admit the behavior above 
(error in case (ii), whereas it is working in case (i)) because n is a 
(Name), and so is not instance of Lift. Thus we are compelled to use lift 
instead of [||] (although the behavior is about the same for both in simple 
examples, as shown in my example above for u).

I do not understand the exact reason for that, but I can do without; and 
maybe it is better, because I am very probably not enough experienced to 
understand the details (and the reason is perhaps not trivial when I read 
Oleg who writes that what gives an error above in Haskell works in 
MetaOCaml).

What is strange is that:
* in the version using lift, the definition of lift asks for the output of 
(nameBase n) to be an instance of Lift, what is the case because it is a 
string (cf my previous post in this thread).
* whereas in the second version, we ask for n, not (nameBase n), to be an 
instance of Lift.

Anyway, if we admit your axiom as granted, then we can also admit that the 
following version does not work (version of my initial post):

  pr :: Name - ExpQ
  pr n = [| putStrLn $ (nameBase n) ++  =  ++ show $(varE n) |]

Thanks,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] typeclass constraints

[TP]

Hi everybody,


There is something I do not understand in the way typeclass constraints are 
inferred.


1/ Take the following function definition:

sum' [] = []
sum' (x:xs) = x + sum' xs

GHCI correctly gives:

 :t sum'
sum' :: Num [a] = [[a]] - [a]

So it has inferred that the type list has to be an instance of Num for sum' 
to be able to work. It will give an error if we try to use sum' without 
implementing the instance.


2/ Now, take the following definition:


{-# LANGUAGE TemplateHaskell #-}

import Language.Haskell.TH
import Language.Haskell.TH.Syntax

p :: a - ExpQ
p n = [| show n |]


We obtain an error if we try to load it in GHCI:

No instance for (Lift a) arising from a use of `n'
Possible fix:
  add (Lift a) to the context of
the type signature for p :: a - ExpQ
In the first argument of `show', namely `n'
In the Template Haskell quotation [| show n |]
In the expression: [| show n |]

And indeed, if we use instead:


{-# LANGUAGE TemplateHaskell #-}

import Language.Haskell.TH
import Language.Haskell.TH.Syntax

p :: Lift a = a - ExpQ
p n = [| show n |]


it works correctly.


Why GHC is able to infer the typeclass constraint (Num a) in 1/, but not 
(Lift a) in 2/?


Thanks in advance,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] typeclass constraints

[TP]

Adam Gundry wrote:

 If you leave off the type signature, as you did for sum', the
 right thing will be inferred.

Thanks Adam and Ivan. Very stupid question...

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] reasons why Template Haskell does not propose something similar to Python exec() or eval()

[TP]

Hi everybody,

I continue to learn and test Template Haskell (one more time thanks to John 
Lato for his post at:

http://www.mail-archive.com/haskell-cafe@haskell.org/msg106696.html

that made me understand a lot of things).

I have a question about the way Template Haskell is working. Why Template 
Haskell does not propose something similar to Python (or bash) exec() or 
eval(), i.e. does not offer the possibility to take a (quoted) string in 
input, to make abstract syntax in output (to be executed later in a splice 
$()).
For example, in Python, to make an affectation 'a=a' programatically, I 
can simply do (at runtime; even if I am here only concerned with what 
Template Haskell could do, i.e. at compile time):
 def f(s): return '%s = \'%s\'' % (s,s)
 exec(f(a))
 a
'a'

With Template Haskell, I am compelled to make a function returning the 
abstract syntax corresponding to variable declaration:

ValD (VarP $ mkName s) (NormalB $ LitE $ StringL s)

(see complete example in Post Scriptum).
This works fine, but it is less direct. I am sure that the Template Haskell 
approach has many advantages, but I am unable to list them. I think it is 
important to have the reasons in mind. Could you help me?

Thanks in advance,

TP


PS: the complete Haskell example:

---
module MakeVard where
import Language.Haskell.TH

makeVard :: Monad m = String - m [Dec]
-- Equivalent to %s = \%s\
makeVard s = return [ ValD (VarP $ mkName s) (NormalB $ LitE $ StringL s) [] 
]
---

tested by

---
{-# LANGUAGE TemplateHaskell #-}
import MakeVard

$(makeVard a)

main = do

print a
---

resulting in
$ runghc -ddump-splices test.hs 
test_makeVar.hs:1:1: Splicing declarations
makeVard a
  ==
test_makeVar.hs:4:3-14
a = a
a


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Template Haskell: let statement in a splice put in the main = do part of a program?

[TP]

Hi,

I continue to test Template Haskell, and I have some difficulties to use a 
splice $() in a do contained in the main part of a program. Here is an 
example. I want to make a splice that does `let a=a` in my code.


$ cat MakeLetStatement.hs

{-# LANGUAGE TemplateHaskell #-}

module MakeLetStatement where

import Language.Haskell.TH

makeLetStatement :: String - ExpQ
makeLetStatement s = return $ DoE $ [ LetS $ [ ValD (VarP $ mkName s)
(NormalB $ LitE $ StringL s) [] ]]


$ cat test_MakeLetStatement.hs

{-# LANGUAGE TemplateHaskell #-}

import MakeLetStatement

main = do

$(makeLetStatement a)
-- print a


Note I have commented print a because otherwise I obtain Not in scope: 
`a' that shows that `a` has not been defined correctly, but does not show 
whether my splice has been correctly expanded (I use --dump-splices GHC 
option, but it seems it is not working for splices in the main = do part).

I obtain:
$ runghc -ddump-splices test_MakeLetStatement.hs 

test_MakeLetStatement.hs:7:3:
Illegal last statement of a 'do' block:
  let a = a
(It should be an expression.)
When splicing a TH expression: do let a = a
In a stmt of a 'do' block: $(makeLetStatement a)
In the expression: do { $(makeLetStatement a) }
In an equation for `main': main = do { $(makeLetStatement a) }

That shows that my splice has been correctly expanded: we have `let a = 
a`. However, what happens is the same as in the following dummy script, we 
have in fact defined a do inside the first do (with DoE), and so we 
obtain an error because the last statement in a do block should be an 
expression.

main = do
do let a = a
print a


So my code does not work, without surprise, but in fact my problem is to 
transform a LetS statement:

http://www.haskell.org/ghc/docs/latest/html/libraries/template-haskell-2.8.0.0/Language-Haskell-TH.html#v:LetS

that has type Stmt, in an ExpQ that seems to be the only thing that we can 
put in a splice. I have found that it can only be done by doE (or DoE) and 
compE (or CompE) according to 

http://www.haskell.org/ghc/docs/latest/html/libraries/template-haskell-2.8.0.0/Language-Haskell-TH.html#v:doE

But doE is not a solution as we have seen above, and compE is to construct 
list comprehensions, which is a different thing.

So, is there any solution to my problem?

Thanks in advance,

TP



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Template Haskell: let statement in a splice put in the main = do part of a program?

[TP]

Brandon Allbery wrote:

 main = do

 $(makeLetStatement a)
 -- print a

 
 Is that the actual indentation you used? Because it's wrong if so, and the
 error you would get is the one you're reporting. Indentation matters in
 Haskell.

Yes, it matters, but not after main = do: all the lines can start at the 
beginning of the line. Am I wrong? Or do I not understand what you say?

 In an equation for `main': main = do { $(makeLetStatement a) }

 
 You cannot *end* a do with a let-statement; it requires something else
 following it. You have nothing following it, as shown by the above
 fragment from the error message.

Yes, I have explained why: to be able to see the evaluation of the splice; 
otherwise I obtain Not in scope: `a' if I uncomment -- print a at the 
end of my code; I have explained everything in my initial post.

TP



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] reasons why Template Haskell does not propose something similar to Python exec() or eval()

[TP]

Tobias Dammers wrote:

 IIRC you can use haskell-src-exts to parse a string into TH AST
 structures. There might even be a quasi-quoter for that; I don't have a
 real computer at hand right more, so you'll need to do some research of
 your own.

Thanks Tobias, it led me to the right path. There is indeed a solution in 
Language.Haskell.Meta:

$ ghci
 :m Language.Haskell.Meta
 parseDecs s=s+1
Right [ValD (VarP s) (NormalB (UInfixE (VarE s) (VarE +) (LitE (IntegerL 
1 []]
 parseExp x+1
Right (UInfixE (VarE x) (VarE +) (LitE (IntegerL 1)))
 :i parseDecs
parseDecs ::
  String - Either String [Language.Haskell.TH.Syntax.Dec]
-- Defined in `Language.Haskell.Meta.Parse'
 :i parseExp 
parseExp :: String - Either String Language.Haskell.TH.Syntax.Exp
-- Defined in `Language.Haskell.Meta.Parse'

Thanks,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Template Haskell: let statement in a splice put in the main = do part of a program?

[TP]

adam vogt wrote:

 TH quotes limited as you've noticed. One way to generate similar code
 is to note that:
 
 do
   let x = y
   z
 
 is the same as let x = y in do z. You can generate the latter with
 something like the following file, but the `a' isn't in scope for the
 second argument to makeLetStatement. The uglier $(dyn a) works,
 though I suppose it's more verbose than manually in-lining the
 variable a.
 
 {-# LANGUAGE TemplateHaskell #-}
 import Language.Haskell.TH
 
 main = $(let
 
 makeLetStatement :: String - ExpQ - ExpQ
 makeLetStatement s rest = letE [ valD (varP (mkName s))
 (normalB $ stringE s) []]
 rest
 
 in makeLetStatement a [| print $(dyn a) |] )

Thanks Adam.
Unfortunately, this solution is not satisfying because the goal is to put 
only one mention to a in the main part, putting all the repetitive code 
and ExpQ's in a separate module. Tonight, I've tried hard one more time 
without more success.
Maybe I have to stick to non-let expressions in the main part of a script, 
when it comes to TH. It should nevertheless allow me to call functions, make 
tests, etc.

Thanks,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] using default declaration for overloaded numeric operations

[TP]

Hi,

I try to develop an embedded domain specific language in Haskell.
I don't want to type ::Rational all the time, so I try to use a default 
declaration for my types.

This works correctly in this simple example:

--
default (Integer, Double) -- default default

mag :: Float - Float - Float
mag x y = sqrt( x^2 + y^2 )

main = do

print $ mag 1 1
--

Indeed we obtain sqrt(2) as a result. If we replace the default declaration 
by:
default ()
, we obtain errors at compilation as expected: the type of `2` is ambiguous.

Now let us consider a more complicated example:

--
{-# LANGUAGE FlexibleInstances #-}
import Prelude hiding ((^^))
import Data.Ratio

default (Integer, Rational, Double)

class (Num a) = Foo a where
(^^) :: Num b = b - a - b

instance Foo Rational where
(^^) x r = x ^ n
where n = 2*numerator r -- dummy calculation

instance Foo Integer where
(^^) x n = x ^ n

mag :: Float - Float - Float
mag x y = sqrt( x ^^ 2 + y ^^ 2 )

main = do
print $ mag 1 1
--

I would expect it to work correctly, but we obtain errors concerning the 
ambiguous type of `2`.
Why?
How to make my default declaration work?
And if I want to give the priority to `Rational` instead of `Integer`? 
Indeed, this should be possible because we don't get any error below.

$ ghci
 import Data.Ratio
 2::Rational
2 % 1

Thanks in advance,

TP

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] type-level integers, type-level operators, and most specific overlapping instance

[TP]

Hi everybody,

I encouter some problem in my code in the following simple example: two 
instances overlap for the multiplication sign `*`. The 
`OverlappingInstances` extension is of no help because it seems GHC does not 
look at the instance context to decide which instance is the most specific.

file:///usr/share/doc/ghc-doc/html/users_guide/type-class-
extensions.html#instance-overlap

How to make GHC realize that in the second instance below, the instance 
context is not satisfied, such that the first instance has to be used? 
(Indeed, a Scalar is a `Tensor 'Zero`, so the strict inequality `'Zero : n` 
is not satisfied in the context).


{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}

import Prelude hiding ((*))

data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )

type family (m::Nat) : (n::Nat) :: Bool -- Here Bool is a kind.
type instance m : 'Zero = 'False
type instance 'Zero : ('Succ n) = 'True
type instance ('Succ m) : ('Succ n) = m : n

data Tensor :: Nat - * where
Tensor :: Tensor order
Mult   :: Scalar - Tensor order - Tensor order
deriving instance Show (Tensor order)

type Scalar = Tensor 'Zero

class Multiplication a b c | a b - c where
(*) :: a - b - c

instance Multiplication Scalar (Tensor n) (Tensor n) where
s * t = Mult s t

instance (('Zero : n) ~ 'True) =
 Multiplication (Tensor n) Scalar (Tensor n) where
t * s = Mult s t

main = do

let s = Tensor :: Scalar
let a = s*s
print a


that yields at compilation:

Overlapping instances for Multiplication
Scalar Scalar (Tensor 'Zero)
  arising from a use of `*'
Matching instances:
  instance [overlap ok] Multiplication Scalar (Tensor n) (Tensor n)
-- Defined at 
test_overlapping_instance_with_typelevelinteger_test.hs:31:10
  instance [overlap ok] ('Zero : n) ~ 'True =
Multiplication (Tensor n) Scalar (Tensor n)
-- Defined at 
test_overlapping_instance_with_typelevelinteger_test.hs:34:10
In the expression: s * s
In an equation for `a': a = s * s
In the expression:
  do { let s = ...;
   let a = s * s;
   print a }


Thanks in advance,

TP

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type-level integers, type-level operators, and most specific overlapping instance

[TP]

adam vogt wrote:

 You can add another instance to cover the case that everything is zero.
 Then you don't need the :. Also it's convenient to arrange for the
 a,b,c to be the argument to Tensor, as given below:
 
 class Multiplication a b c | a b - c where
 (*) :: Tensor a - Tensor b - Tensor c
 
 instance Multiplication Zero Zero Zero where
 s * t = Mult s t
 instance Multiplication Zero n n where
 s * t = Mult s t
 instance Multiplication n Zero n where
 t * s = Mult s t

Thanks a lot Adam. It is a pity I did not think to this solution myself. 
Below is the full code for a working version (however still using a more 
general definition of multiplication compared to yours).

But I have still a question: is the behavior of GHC correct in the example 
of my initial post? It is OK it does not look at the most specific instance 
by examining the instance context? Is it OK, or is it a deficiency?

Thanks,

TP

-
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}

import Prelude hiding ((*))

data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )

data Tensor :: Nat - * where
Tensor :: Tensor order
Mult   :: Scalar - Tensor order - Tensor order
deriving instance Show (Tensor order)

type Scalar = Tensor 'Zero

class Multiplication a b c | a b - c where
(*) :: a - b - c

instance Multiplication Scalar Scalar Scalar where
s * s' = Mult s s'

instance Multiplication Scalar (Tensor n) (Tensor n) where
s * t = Mult s t

instance Multiplication (Tensor n) Scalar (Tensor n) where
t * s = Mult s t

main = do

let s = Tensor :: Scalar
let a = s*s
print a

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type-level integers, type-level operators, and most specific overlapping instance

[TP]

TP wrote:

 But I have still a question: is the behavior of GHC correct in the example
 of my initial post?

See here:

http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/type-class-extensions.html#instance-overlap


When matching, GHC takes no account of the context of the instance 
declaration (context1 etc). GHC's default behaviour is that exactly one 
instance must match the constraint it is trying to resolve.


My misunderstanding came from a confusion between a context and a 
constraint. The context is what is before the =, and the constraint is 
what is after, i.e. the main part of the instance declaration.

This is the reason why my context using an inequality test on type-level 
integers was not taken into account: if I understand well there must be only 
one instance that matches the constraint, independently from the contexts, 
before GHC checks that the instance context is indeed respected.

The OverlappingInstances option only helps to have only one matching 
instance (independently from the contexts): if several instances match, but 
there is a more specific one, GHC selects this one and then checks the 
corresponding instance context.

Thanks,

TP

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type-level integers, type-level operators, and most specific overlapping instance

[TP]

adam vogt wrote:

 I think context and constraint mean the same thing. The haskell report
 uses the word context for
 http://www.haskell.org/onlinereport/decls.html for the whole list
 and constraint for one part of that list (Eq a). With the extension
 -XConstraintKinds both of those are called Constraint. In other words:
 
 instance Context = InstanceHead

 instance (Constraint, Constraint2) = InstanceHead

This is indeed more in accordance with what I believe to be a context or a 
constraint. But, it seems that in this page

http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/type-class-extensions.html#instance-overlap

the vocabulary is different:


  instance context1 = C Int a where ...  -- (A)
  instance context2 = C a   Bool  where ...  -- (B)
  instance context3 = C Int [a]   where ...  -- (C)
  instance context4 = C Int [Int] where ...  -- (D)

The instances (A) and (B) match the constraint C Int Bool, but (C) and (D) 
do not. When matching, GHC takes no account of the context of the instance 
declaration (context1 etc).

[...]

The -XOverlappingInstances flag instructs GHC to allow more than one 
instance to match, provided there is a most specific one. For example, the 
constraint C Int [Int] matches instances (A), (C) and (D), but the last is 
more specific, and hence is chosen. If there is no most-specific match, the 
program is rejected. 


So, what do I miss? Isn't the vocabulary different here?
And I do not understand what is written if I take your definition (which is 
indeed the definition in the Haskell report).

Thanks in advance,

TP


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe