[Haskell-cafe] working my way through Data.Type.Equality...my head hurts...

[Oliver Charles]

It can be done that way, but just keep in mind that a lot of things are
significantly more complicated than they need to be in Haskell, when
compared to Agda. Idris might be a good option to explore too, as you get
very familiar syntax, but something that's designed from the start for
dependent typing.

On Tue, Jan 13, 2015 at 2:10 PM, Nicholls, Mark <nicholls.mark at vimn.com>
wrote:

> I was thinking of doing it the other way around....
> i.e. get my head around Haskell....then around Haskell's type system
> extensions....then look at agda.
>
>
> CONFIDENTIALITY NOTICE
>
> This e-mail (and any attached files) is confidential and protected by
> copyright (and other intellectual property rights). If you are not the
> intended recipient please e-mail the sender and then delete the email and
> any attached files immediately. Any further use or dissemination is
> prohibited.
>
> While MTV Networks Europe has taken steps to ensure that this email and
> any attachments are virus free, it is your responsibility to ensure that
> this message and any attachments are virus free and do not affect your
> systems / data.
>
> Communicating by email is not 100% secure and carries risks such as delay,
> data corruption, non-delivery, wrongful interception and unauthorised
> amendment. If you communicate with us by e-mail, you acknowledge and assume
> these risks, and you agree to take appropriate measures to minimise these
> risks when e-mailing us.
>
> MTV Networks International, MTV Networks UK & Ireland, Greenhouse,
> Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions
> International, Be Viacom, Viacom International Media Networks and VIMN and
> Comedy Central are all trading names of MTV Networks Europe.  MTV Networks
> Europe is a partnership between MTV Networks Europe Inc. and Viacom
> Networks Europe Inc.  Address for service in Great Britain is 17-29 Hawley
> Crescent, London, NW1 8TT.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150113/da42a0cd/attachment.html>