# MumbleFuzz

Member

120

188 Neutral

• Rank
Member
1. ## Am I the only one?

Quote:Original post by Sneftel If you add recursion (via a fixed-point operator), halting becomes undecidable. You can't have it both ways. Indeed, which is why I said it's not possible. I was just checking my earlier reasoning, which I thought Rebooted disagreed with. [Edited by - MumbleFuzz on November 28, 2007 7:17:37 AM]
2. ## Am I the only one?

Quote:Original post by Rebooted You can then look a program's type and see whether or not it uses general recursion, so you have a proof that a certain class of programs in the language terminate. Quote:Original post by Daerax Although I do think that turing completeness is overhyped, a language need not have this feature to be sufficient for nearly all computational needs. Like say the now defunct Charity. Interesting... I've never really studied the different classes of recursive functions, so I've always just taken Turing-completeness to be a benchmark for expressability. It's something I'll have to look into further [smile].
3. ## Am I the only one?

Quote:Original post by Rebooted That's true, STLC is not turing complete. It's the simplest type system that proves programs terminate, but there are others (it's not equivalent to solving the halting problem). I must admit I've never studied the formal properties of these languages in depth, but I was rather under the impression that recursion was the only feature missing from STLC which prevented it from being Turing-complete. Therefore, if one extended it with recursion, and then (hypothetically speaking) proved, for any program and input, whether or not a program terminates, would one not then have a solution to the halting problem? Perhaps I was a little vague, but this is what I had in mind.
4. ## Am I the only one?

Quote:Original post by Daerax Quote:Original post by MumbleFuzz Quote:Original post by Rebooted Can you show me a "dynamic" type system that can prove a program terminates (I think that might be difficult [smile]) I think that's a slightly unfair question, seeing as the simply-typed lambda calculus isn't Turing-complete... Where did you read this? I am certain that lambda -> is turing complete. perhaps you misattributed something on a constructive type theory sans recursion? For example a language which builds on a simply typed lambda calc is Haskell or Ocaml. The untyped lambda calculus is Turing-complete, but the simply typed lambda calculus by itself lacks recursion. This is because a fixed point combinator (which can be defined in terms of the untyped calculus) is impossible to type in this system. That's not to say you can't extend the calculus with new language features which are equivalent -- but at this point proof of termination is no longer possible (or else you would have solved the halting problem). Perhaps you already knew this and assumed "the simply typed lambda calculus" to refer to the language extended with, say, a fix operator. I don't believe that's standard in the literature, however, and it certainly isn't the language linked to by Rebooted. [Edited by - MumbleFuzz on November 27, 2007 4:14:10 AM]
5. ## Am I the only one?

Quote:Original post by Rebooted Can you show me a "dynamic" type system that can prove a program terminates (I think that might be difficult [smile]) I think that's a slightly unfair question, seeing as the simply-typed lambda calculus isn't Turing-complete... (Unless it turns out, for some curious reason, that most popular dynamically-typed languages aren't either. To be honest I really have no idea [smile].)
6. ## Do you still make simple errors?

As far as I know, today was the first time I've ever written this: if (foo = bar) { ... } Luckily it didn't take too long to spot the missing equality, 'cos it was the termination condition for a loop and resulted in a massive dialog appearing rapidly and repeatedly for no apparent reason. Generally, though, the only mistakes I make these days are design decisions. The syntax (of the languages I use regularly, anyway) is mostly second nature.

8. ## some help on my programming language

Quote:Original post by Nathan Baum That doesn't make sense. It's true that a multiple assignment isn't a tuple, but that's because "multiple assignment" and "tuple" describe entirely different things. You may as well complain that a function call isn't a string. That was precisely my point. EDIT: But you're right to include your alternative #3. I was so confused by the boxing construct at first that I forgot what the original tuple assignment was for. [Edited by - MumbleFuzz on July 27, 2007 9:48:01 AM]
9. ## some help on my programming language

Quote:I added this operator to make it so that I can easily make templated containers. For example the list template takes a type as a template parameter for its element type. Using the boxing operator allows you to store boxed tuples in a list.Ah. Do I take it you don't have typing rules for tuples? Is there any particular reason for this? EDIT: Oh. I see what you've done. In your example, you seem to be taking (x,y) = (5,6) to be a shorthand for x = 5; y = 6;. Which is neat: multiple assignments are groovy. What they are not, however, is tuples. I believe you are mixing the two. Your problem would therefore be best solved in one of two ways: 1. Keep tuples and find a new syntax for multiple assignments. 2. Keep your current syntax for multiple assignments and discard tuples. Once you've got records, you've effectively got tuples anyway. As a final note, I think you would have noticed this for yourself had you given tuples a typing rule. And in any case, a language without typing rules for even a single term cannot be type safe, so unless you have typing rules for every construct, you may as well remove the type system altogether. [Edited by - MumbleFuzz on July 26, 2007 3:48:54 PM]
10. ## some help on my programming language

I'm not sure I entirely follow. What is the purpose of the boxing construct when you already have tuples? In your example...int x, int y; (x,y)=(5,6)...presumably the type of (x,y) is something like (int, int) or int * int? If that is the case, then surely [int, int]m and (int, int)m would declare variables that behave in the same way (modulo the type)? So then why not keep the boxing notation solely for records (which effectively generalize tuples by naming the fields)? Finally, I believe that [int x, int y] && [int y, int z] should not be a well typed term. You should require that the sets of names of fields in two record types be disjoint when the records are combined in this manner.
11. ## Equivalent of OCaml 'when' clause in Haskell?

Quote:Original post by Rebooted This should work: eval :: Term -> Term eval (App (Abs t12), v2) | isval v2 = subst 0 v2 t12 eval (App (v1, t2) | isval v1 = App (v1, eval t2) eval (App (t1, t2)) = App(eval t1, t2) Yup. Fantastic! Many thanks, Rebooted.
12. ## Equivalent of OCaml 'when' clause in Haskell?

I'm trying to throw together a small language (currently just the untyped lambda calculus) interpreter. Eventually I'll have to write it in OCaml, but for the time being I thought I'd try Haskell. It's been a while since I used the language, though, and I'm trying to remember if there's a way to write the following function: eval :: Term -> Term eval (App (Abs t12), v2) when isval v2 = subst 0 v2 t12 eval (App (v1, t2) when isval v1 = App (v1, eval t2) eval (App (t1, t2)) = App(eval t1, t2) (The type Term is given by: data Term = Var Int | Abs Term | App (Term, Term).) The equivalent function in OCaml would match the first line of the definition only when the predicate isval v2 is true. Is there a similar clause in Haskell, or an otherwise neat way to write the function? Currently the best I can come up with is: eval :: Term -> Term eval (App(t1,t2)) | isval t1 && isval t2 = subst 9 t2 t12 | isval t1 = App(t1, eval t2) | otherwise = App(eval t1, t2) where t12 = get_abs_term t1 get_abs_term (Abs t12) = t12 which I suppose is ok; but as the eval function becomes more complex (which it will do), I suspect that more and more definitions will have to be given in the where clause, and I think readability will suffer. Any suggestions on how I might write it? Like I say, I'm not too familiar with Haskell, so I'm probably missing something simple.
13. ## Dynamic 3D Arrays

Quote:Original post by AltecZZ I get this error on the first line: unsigned int *** imageData = unsigned int ** [IMAGE_SIZE]; VS2005 complains about type 'unsigned int' unexpected Try: unsigned int *** imageData = new unsigned int ** [IMAGE_SIZE];

Quote:Original post by chollida1 Quote:Original post by MumbleFuzz I'm quite a fan of Introduction To Functional Programming by Richard Bird. Despite what the reviews say (they claim it's not a book for beginners), I found it to be a good introduction to a language I'd never used before. I found that "Introduction to Functional programming" Did give a decent background to functional programming but it read too much like a university text for my liking and its more expensive:) IMHO If you want to learn Haskell that's not the book for you as Haskell is just the vehicle he uses to get the theorey across. Having said that, if your goal is to learn the theory of functional programming rather than Haskell itself then perhaps that book could be a winner? I guess that's probably true -- I was more interested in the theory of functional programming as a paradigm at the time (in fact, I was taking Bird's course). Since I tend to program in imperative languages, it was a refreshing change, and extremely insightful.