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

[Jan Stolarek]

Why not, if you feel that works for you. But in Agda you don't need things like Type Families or 
some fancy encodings like singletons - you can use the same functions at term and type levels.

Janek

Dnia wtorek, 13 stycznia 2015, Nicholls, Mark napisał:
> 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.