Questions tagged [bounded-quantification]
9 questions
11
votes
1 answer
Scala converting recursively bounded type parameter (F-bounded) to type member
How would I convert:
trait Foo[A <: Foo[A]]
to a type member?
I.e., I want something along the lines of the following:
trait Foo {
type A <: Foo {type A = ???}
}
but I am having difficulty because the name A is already taken within the type…
Alex DiCarlo
- 4,851
- 18
- 34
8
votes
2 answers
Cannot implement representation type as type member
While cracking my head over another question, I came across different riddles which seem related. This is one of them:
trait Sys[S <: Sys[S]] {
type Peer <: Sys[Peer]
}
trait Fenced {
type Peer <: Sys[Peer]
}
def makeFence[S <: Sys[S]] = new…
0__
- 66,707
- 21
- 171
- 266
6
votes
2 answers
Understanding "type arguments do not conform to type parameter bounds" errors in Scala
Why don't the following work?
scala> abstract class Foo[B<:Foo[B]]
defined class Foo
scala> class Goo[B<:Foo[B]](x: B)
defined class Goo
scala> trait Hoo[B<:Foo[B]] { self: B => new Goo(self) }
:9: error: inferred type arguments [Hoo[B]…
Yang
- 16,037
- 15
- 100
- 142
5
votes
2 answers
Existential type or type parameter bound failure
I have an F-bounded type Sys:
trait Sys[S <: Sys[S]]
And some trait which take it as type parameter:
trait Foo[S <: Sys[S]]
Suppose I have a method to be invoked with a Foo:
def invoke[S <: Sys[S]](foo: Foo[S]) = ()
Suppose I have a model update…
0__
- 66,707
- 21
- 171
- 266
3
votes
4 answers
F-bounded quantification through type member instead of type parameter?
I would like to move a type parameter to a type member.
This is the starting point which works:
trait Sys[S <: Sys[S]] {
type Tx
type Id <: Identifier[S#Tx]
}
trait Identifier[Tx] {
def dispose()(implicit tx: Tx): Unit
}
trait Test[S <:…
0__
- 66,707
- 21
- 171
- 266
1
vote
1 answer
Dafny as a SAT-QBF solver is not giving right results
I am trying to get the habit to use Dafny as a friendly SAT-QBF solver for some simple formulae, since doing it in, for instance, Z3 is too uncomfortable.
The context for this is that I have implemented Cooper's algorithm for quantifier elimination…
Theo Deep
- 666
- 4
- 15
1
vote
1 answer
CVC4: settings to syntheize functions over bools with quantifiers?
I'm currently using CVC4 to solve formulas of the following form:
exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk)
Here, the f1...fn are functions from some number of Bool to Bool, and the
b1...bk are boolean…
jmite
- 8,171
- 6
- 40
- 81
1
vote
1 answer
Can't use a type projection to a recursive (f-bounded) type
I am getting a type error which I don't understand, when using a projection from one f-bounded type to another. It might be related to an earlier question but I'm not sure.
The setup is simple:
trait Foo[F <: Foo[F]] {
type I <: Foo[I]
}
That is,…
0__
- 66,707
- 21
- 171
- 266
0
votes
1 answer
Scala loses track of related types when concatenating (projecting) type members
I am walking around a problem, and I found a new strange problem with type projections and abstract types. Say I have a system which spawns transactions, and there is a peer system to which I want to bridge. The following looks good to me:
trait…
0__
- 66,707
- 21
- 171
- 266