On 14 Jun 2015 6:48 am, "Matt Oliveri" <atma...@gmail.com> wrote: > > 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.
Well I can't think of an easy way to do it in Haskell. Type definitions get lifted like this: type(bool, true). type(bool, false). So the predicate would be: has_two(X) :- type(X, Y), type(X, Z), dif(Y, Z). Used as in: test :: has_two a => a -> a Keean. > > 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
_______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
