It was a contrived example, I don't know any use to program verification off the top of my head. However it's meaning, that I gave in English, should be intuitively clear.
(HasTwo T) should be true, where T is a type, if and only if T has at least two elements. For example, (HasTwo bool) is true. (HasTwo nat) is true. (HasTwo unit) is false. (HasTwo T), where T is an abstract type, is unknown. I repeat that it's no big deal if your system can't express this predicate. On Sun, Jun 14, 2015 at 1:24 AM, Keean Schupke <ke...@fry-it.com> wrote: > > What are you trying to do with HasTwo? Can you give me an example of its > use? > > On 13 Jun 2015 10:43 pm, "Matt Oliveri" <atma...@gmail.com> wrote: >> >> Is this supposed to be HasTwo? I don't see how it can be right. You >> are using type classes for predicates, correct? And HasTwo is a >> predicate. But has_two is not a type class. >> >> Informally, the ingredient you seem to be leaving out is an >> existential quantifier. >> >> On Sat, Jun 13, 2015 at 7:25 AM, Keean Schupke <ke...@fry-it.com> wrote: >> > has_two :: dif a b => (a, b) >> > has_two x y = (x, y) >> > >> > On 13 Jun 2015 12:14 pm, "Matt Oliveri" <atma...@gmail.com> wrote: >> >> Although I'm still curious whether HasTwo can be defined as a type >> >> class... _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
