Talk:Crowbar

<elliott>  Nat: cover from Number {
<elliott>    rule \A (a: Nat | a >= 0)
<elliott>  }
<elliott> nddrylliog: you want that to be "a: Number"
<Phantom_Hoover> elliott, no.
<elliott> Phantom_Hoover: ?
<Phantom_Hoover> Well, I suppose both would work.
<elliott> not really
<elliott> the way it is now is circular
<elliott> which is just weird
<elliott> all nats are >= 0
<elliott> except that it's only because of that rule that it's valid
<elliott> which then makes it a tautology
<elliott> I'd definitely make it "a: Number"

—ehird 17:32, 5 February 2011 (UTC)

<Phantom_Hoover> It's universal wossname, so "Number" doesn't make much sense.
<elliott> Phantom_Hoover: "Nat: cover from Number"
<elliott> Number is the type that Nat is covering.
<elliott> Duh.
<Phantom_Hoover> Covering?
<elliott> RTFLanguage
<Phantom_Hoover> And yes, I know that.
<elliott> Number is just integer there I think.
<elliott> So, uh.
<elliott> It should definitely be Number.
<elliott> It's a predicate that tells you whether a Number is a valid Nat.
<Phantom_Hoover> Universal quantification is not the right thing to have, then.
<elliott> Phantom_Hoover: Well, possibly.

—e–"everybody who disagrees me is working on mistaken assumptions"–hird 17:36, 5 February 2011 (UTC)

Indeed, I think that it should actually just be a function from a Number to a boolean (really a proposition, but I think all your propositions are decidable here, and using booleans is much simpler to implement). —ehird 17:39, 5 February 2011 (UTC)

btw, I'm not sure the "Index: cover from Nat" thing actually uses dependent types. —ehird 17:41, 5 February 2011 (UTC)

Well I don't really like using universal quantification, I guess I was just trying to look smart or something. "this >= 0" is fine by me (this being the Number, and the comparison expression being the boolean, hence a proposition) Nddrylliog 22:03, 6 February 2011 (UTC)

Esolang?

Is this supposed to be an esoteric programming language, or not? It doesn't really "feel" like one to me, and it's not described as one, but maybe that was an oversight and maybe there's something I'm missing. --Chris Pressey 00:25, 14 February 2011 (UTC)

It's an experimental language created to play with concepts rather than be used practically; that's esoteric enough in my book. Phantom Hoover 09:44, 23 February 2011 (UTC)

Computational class

Assuming that tail-call elimination is performed, it's trivially TC. Phantom Hoover 09:43, 23 February 2011 (UTC)

Um maybe there's something specific about Crowbar, but in general I don't see how tail-call elimination is relevant to TC-ness unless a language has an explicit stack limit. --Ørjan 13:20, 23 February 2011 (UTC)

Well, yeah, that was a misphrasing. "Unlimited recursion" is what I was trying to say. 92.233.174.117 15:48, 23 February 2011 (UTC)