Re: type-directed programming

From: Claus Reinke <claus.reinke_at_talk21.com>
Date: Fri, 15 Dec 2006 13:04:33 +0000

>I don't think so. You can replace "where x free" with "where x = _|_"
>and Curry will still infer the type for you:
>
>cursor = mz
> where
> plus :: Nat -> Nat -> Nat
> plus = prec mz ms
> mz = undefined
> ms = undefined
>
>undefined = undefined
>
>primrec> :t cursor
>cursor :: Nat -> Nat

I wasn't sure about the typing of free variables in the earlier versions, but
this definitely looks wrong, unless Curry deviates from Haskell more than
I thought (aren't where-bindings polymorphic, like let-bindings?).

>Interestingly, Haskell does not! If we load this in ghci, we get:
>
>*Main> :t cursor
>cursor :: a

This looks right: mz is polymorphic, and that a specific substitution instance
is needed to make prec typecheck has no effect on its most general type.

Here is Bernd's variant translated to Haskell, using lambda-binding instead
of let-binding for the things whose types we want information on:

    data Nat = Z | S Nat

    foldNat :: a -> (a -> a) -> Nat -> a
    foldNat z _ Z = z
    foldNat z s (S x) = s (foldNat z s x)

    cursor z s = (z,s)
      where
      plus :: Nat -> Nat -> Nat
      plus = foldNat z s

no "free", just parameterized by the unknowns z and s. now we can load
this into GHCi, and get:

    *Main> :t cursor undefined undefined
    cursor undefined undefined :: (Nat -> Nat, (Nat -> Nat) -> Nat -> Nat)

undefined is still polymorphic, but being lambda-bound inside of cursor, all
occurrences of z share the same type, so we get more specific information.

Claus


_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fri Dec 15 2006 - 15:05:23 CET

This archive was generated by hypermail 2.3.0 : Mon Sep 16 2019 - 07:15:05 CEST