Re: Another typing question

[Samuel E . Moelius III]

On Wednesday, August 6, 2003, at 06:15 AM, C T McBride wrote:

This is why most sensible dependent type theories have a hierarchy of
universes behind the scenes. You can think of * in Haskell as the lowest
universe, inhabited by types.
Why wouldn't terms be the lowest universe?

Sam Moelius

___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: Writing a counter function

[Samuel E. Moelius III]

 No. But I want to generate an irregular series, which I determine the
 intervals between two consecutive numbers myself. E.g:

 let (num1, next1) = (counter 5)
 (num2, next2) = (next1 100)
 (num3, next3) = (next2 50) in
 [num1,num2,num3]

 Will have the numbers [5, 105, 155].

Here's another not-exactly-what-you-wanted solution.  :)

If you don't mind changing your example to

let (num1, next1) = out (counter 5)
(num2, next2) = out (next1 100)
(num3, next3) = out (next2 50) in
[num1,num2,num3]

then, you can do this:

newtype Counter = MkCounter Int

counter :: Int - Counter
counter n = MkCounter n

out :: Counter - (Int,Int - Counter)
out (MkCounter n) = (n,MkCounter . (n +))

Sam Moelius

___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: Writing a counter function

[Samuel E. Moelius III]

 No. But I want to generate an irregular series, which I determine the
 intervals between two consecutive numbers myself. E.g:

 let (num1, next1) = (counter 5)
 (num2, next2) = (next1 100)
 (num3, next3) = (next2 50) in
 [num1,num2,num3]

 Will have the numbers [5, 105, 155].

Here's another not-exactly-what-you-wanted solution.  :)

If you don't mind changing your example to

let (num1, next1) = out (counter 5)
(num2, next2) = out (next1 100)
(num3, next3) = out (next2 50) in
[num1,num2,num3]

then, you can do this:

newtype Counter = MkCounter Int

counter :: Int - Counter
counter n = MkCounter n

out :: Counter - (Int,Int - Counter)
out (MkCounter n) = (n,MkCounter . (n +))

Sam Moelius

___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Using type

[Samuel E. Moelius III]

I apologize if this question has been asked before...

It seems to me the following code should be legal:

type Thing m = m ()

type Const a b = a

f :: Thing m - Thing m
f x = x

test :: Thing (Const Int) - Thing (Const Int)
test = f

However, GHC gives the following error:

 Couldn't match `Thing m' against `Thing (Const Int)'
 Expected type: Thing m
 Inferred type: Thing (Const Int)
 Expected type: Thing (Const Int) - Thing (Const Int)
 Inferred type: Thing m - Thing m

But if you change the definition of Const

newtype Const a b = MakeConst a

the code compiles fine.

Is this the desired behavior?

Is it the case that when you have quantification of a type variable of 
kind * - * (in this case, m), that variable may only become bound to a 
type constructor?

Sam Moelius

___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: beginner's questions - fix f

[Samuel E . Moelius III]

 Function fix is a so-called fixpoint operator. Theory says that you can
 formulate any computable function using only non-recursive definitions
 plus fix.

Could someone point me toward a proof of this?

Furthermore, can any computable function be expressed in this form:

fix u

where u is some non-recursive term?

Sam Moelius

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell