Re: [Haskell-cafe] About "Fun with type functions" example

On Nov 19, 2010, at 1:07, Daniel Peebles wrote:
The best you can do with fromInt is something like Int -> (forall n. (Nat n) => n -> r) -> r, since the type isn't known at compile time.
Or you put it in the type class as fromInt :: Int -> n and do in Zero: fromInt _ = Zero and in the other: fromInt _ = Succ $ fromInt (undefined :: n). Shouldn't that work, too?
On Thu, Nov 18, 2010 at 2:52 PM, Arnaud Bailly
wrote: Thanks a lot, that works perfectly fine! Did not know this one... BTW, I would be interested in the fromInt too.
Arnaud
On Thu, Nov 18, 2010 at 8:22 PM, Erik Hesselink
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
wrote: Hello, I am trying to understand and use the Nat n type defined in the aforementioned article. Unfortunately, the given code does not compile properly:
[snip]
instance (Nat n) => Nat (Succ n) where toInt _ = 1 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Then you can write fromInt 1 :: Zero, and it will type check.
/J
On 19 November 2010 04:42, Bastian Erdnüß
On Nov 19, 2010, at 1:07, Daniel Peebles wrote:
The best you can do with fromInt is something like Int -> (forall n. (Nat n) => n -> r) -> r, since the type isn't known at compile time.
Or you put it in the type class as fromInt :: Int -> n and do in Zero: fromInt _ = Zero and in the other: fromInt _ = Succ $ fromInt (undefined :: n). Shouldn't that work, too?
On Thu, Nov 18, 2010 at 2:52 PM, Arnaud Bailly
Thanks a lot, that works perfectly fine! Did not know this one... BTW, I would be interested in the fromInt too.
Arnaud
On Thu, Nov 18, 2010 at 8:22 PM, Erik Hesselink
wrote: On Thu, Nov 18, 2010 at 20:17, Arnaud Bailly
wrote: Hello, I am trying to understand and use the Nat n type defined in the aforementioned article. Unfortunately, the given code does not compile properly:
[snip]
instance (Nat n) => Nat (Succ n) where toInt _ = 1 + toInt (undefined :: n)
[snip]
And here is the error:
Naturals.hs:16:18: Ambiguous type variable `n' in the constraint: `Nat n' arising from a use of `toInt' at Naturals.hs:16:18-39 Probable fix: add a type signature that fixes these type variable(s)
You need to turn on the ScopedTypeVariables extension (using {-# LANGUAGE ScopedTypeVariables #-} at the top of your file, or -XScopedTypeVariables at the command line). Otherwise, the 'n' in the class declaration and in the function definition are different, and you want them to be the same 'n'.
Erik
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
participants (2)
-
Bastian Erdnüß
-
Jonas Almström Duregård