Hi,
This is rather off-topic but the audience of this list may be the right
one; if there is a more appropriate venue for this question, please let
me know.
Most descriptions of recursive types state that iso-recursive types
(with explicit 'fold' and 'unfold' operators) are easy to typecheck,
Can Fix be made to work with higher-kinded types? If so, would the
following work:
Perfect = /\ A . Fix (L :: * - *) . (A + L (A,A))
Keep in mind I have no idea what the Perfect data structure is
supposed to look like.
-Antoine
On Jan 24, 2008 9:52 AM, Edsko de Vries [EMAIL PROTECTED] wrote:
On Thu, Jan 24, 2008 at 10:06:04AM -0600, Antoine Latter wrote:
Can Fix be made to work with higher-kinded types? If so, would the
following work:
Perfect = /\ A . Fix (L :: * - *) . (A + L (A,A))
Hi,
Thanks for your quick reply. Unfortunately, your solution does not work. For
Fix X. t
Hmm ...
How about:
Perfect :: * - * = Fix (L :: * - *) . /\ A . (A + L (A,A))
unfold Perfect = [L := Fix L . t] t where t = /\ A . (A + L (A,A))
= /\ A . (A + (Fix L . /\ B . (B + L (B,B))) (A,A))
assuming alpha-equality. Because L and (Fix L . t) are of kind (* -
*), the substitution
On Jan24, Antoine Latter wrote:
Can Fix be made to work with higher-kinded types? If so, would the
following work:
Yes, it can.
For a particular A (e.g., Int), List A is a recursive type
Fix X. 1 + (A * X).
List :: type - type is a family of recursive types: if you give it a
type, it gives
On Thu, Jan 24, 2008 at 10:46:36AM -0600, Antoine Latter wrote:
Hmm ...
How about:
Perfect :: * - * = Fix (L :: * - *) . /\ A . (A + L (A,A))
unfold Perfect = [L := Fix L . t] t where t = /\ A . (A + L (A,A))
= /\ A . (A + (Fix L . /\ B . (B + L (B,B))) (A,A))
assuming
This paper, with a pdf available at Patricia Johann's publications page
http://crab.rutgers.edu/~pjohann/
seems to be related.
Initial Algebra Semantics is Enough! Patricia Johann and Neil Ghani.
Proceedings, Typed Lambda Calculus and Applications 2007 (TLCA'07)
Hope that helps.
On Jan
