[Agda] Type decidability

[Dmytro Starosud]

Ok, thanks!

2013/1/23 Dan Rosén <danr at student.chalmers.se>

> A remark, if you want to have something like decidable equality on
> types, you could encode a universe. There is much literature about
> this, one good starting point could be Stevan Andjelkovic's Master's
> Thesis: http://publications.lib.chalmers.se/records/fulltext/146810.pdf,
> see chapter 3 and onwards.
>
> Best,
> Dan
>
> On Mon, Jan 21, 2013 at 8:01 PM, Daniel Peebles <pumpkingod at gmail.com>
> wrote:
> > I'm pretty sure it shouldn't be possible to do that in Idris (if it is,
> it's
> > probably a bug), and I don't think most people want it in Agda either.
> The
> > main reason it's undesriable is that it violates parametricity, which is
> a
> > property most FP people really want.
> >
> >
> > On Mon, Jan 21, 2013 at 12:58 PM, Dmytro Starosud <d.starosud at gmail.com>
> > wrote:
> >>
> >> Hello guys,
> >>
> >> In Idris one can write:
> >>
> >> g : Type -> Bool
> >> g Int = True
> >> g _ = False
> >>
> >> Is it possible to do the same in Agda, in particular:
> >>
> >> type-dec : (A B : Set) -> Dec (A \equiv B)
> >> type-dec = ?
> >>
> >> Thanks in advance!
> >>
> >> _______________________________________________
> >> Agda mailing list
> >> Agda at lists.chalmers.se
> >> https://lists.chalmers.se/mailman/listinfo/agda
> >>
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130123/ec43ca09/attachment.html