Possible to type a function to a particular constructor?
Hi fellow beginners (and everyone else), As an exercise, I'm implementing a simple, untyped lambda calculus: -- a term is a variable, an application, or abstraction (lambda) data T = V String | A (T) (T) | L String (T) deriving (Eq) So I'm writing a function that returns a list of all the free variables in a term and descendants. I can only get it to compile with type: freev :: T -> [T] It'd be nice for the type of that function to be restricted to just variables like: freev :: T -> [V String] -- compile error: "Not in scope: type constructor or class `V'" Is there some way to express that? The error seems to suggest maybe haskell could do it if I'd just say it correctly. I mean, isn't "V String" a type constructor? Thanks, kov
On Sun, May 02, 2010 at 09:54:11AM -0400, Ken Overton wrote:
Hi fellow beginners (and everyone else),
As an exercise, I'm implementing a simple, untyped lambda calculus:
-- a term is a variable, an application, or abstraction (lambda) data T = V String | A (T) (T) | L String (T) deriving (Eq)
So I'm writing a function that returns a list of all the free variables in a term and descendants. I can only get it to compile with type:
freev :: T -> [T]
It'd be nice for the type of that function to be restricted to just variables like:
freev :: T -> [V String] -- compile error: "Not in scope: type constructor or class `V'"
Is there some way to express that? The error seems to suggest maybe haskell could do it if I'd just say it correctly. I mean, isn't "V String" a type constructor?
No, there's no way to do that. V is a data constructor, not a type constructor; V String is not a type. There's no way to express "values of such-and-such a type but restricted only to things built with such-and-such a constructor" without resorting to fancy type tricks, which you don't really need. Instead, I would expect freev to have the type freev :: T -> [String] It's much more usual to have freev just return the *names* of all the free variables. -Brent
Am Sonntag 02 Mai 2010 15:54:11 schrieb Ken Overton:
Hi fellow beginners (and everyone else),
As an exercise, I'm implementing a simple, untyped lambda calculus:
-- a term is a variable, an application, or abstraction (lambda) data T = V String | A (T) (T) | L String (T) deriving (Eq)
So I'm writing a function that returns a list of all the free variables in a term and descendants. I can only get it to compile with type:
freev :: T -> [T]
It'd be nice for the type of that function to be restricted to just variables like:
freev :: T -> [V String] -- compile error: "Not in scope: type constructor or class `V'"
You can't do that, at least not directly.
Is there some way to express that? The error seems to suggest maybe haskell could do it if I'd just say it correctly. I mean, isn't "V String" a type constructor?
No, V is a data constructor of type String -> T. If freev :: T -> [V String] were a correct type signature, you would somewhere have defined a type constructor V of kind (* -> *), like data V a = Nought | An a. You can introduce a newtype for variables, newtype Var = Var String , change the definition of T, data T = V Var | A T T | L String T -- or L Var T, don't know what's better deriving Eq , and then have freev :: T -> [Var] Or you could use a GADT and phantom types, {-# LANGUAGE GADTs, EmptyDataDecls #-} data Var data Compound data T x where V :: String -> T Var A :: T a -> T b -> T Compound L :: String -> T a -> T Compound deriving Eq freev :: T a -> [T Var] freev v@(V _) = [v] freev (A t1 t2) = ... freev (L str t) = ... , but then V "x" == A (V "x") (V "y") would give a type error. Therefore newtype-ing Var would probably be the better method.
Thanks,
kov
Hi Ken, You can additionally try to change your definition of lambda-terms to use parametric types as follows. data T var = V var | A (T var) (T var) | L var (T var) Then you can write `freev` with the following type. freev :: T var -> [var] Sincerely, jan. On Sun, May 02, 2010 at 09:54:11AM -0400, Ken Overton wrote:
Hi fellow beginners (and everyone else),
As an exercise, I'm implementing a simple, untyped lambda calculus:
-- a term is a variable, an application, or abstraction (lambda) data T = V String | A (T) (T) | L String (T) deriving (Eq)
So I'm writing a function that returns a list of all the free variables in a term and descendants. I can only get it to compile with type:
freev :: T -> [T]
It'd be nice for the type of that function to be restricted to just variables like:
freev :: T -> [V String] -- compile error: "Not in scope: type constructor or class `V'"
Is there some way to express that? The error seems to suggest maybe haskell could do it if I'd just say it correctly. I mean, isn't "V String" a type constructor?
Thanks,
kov
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
-- Heriot-Watt University is a Scottish charity registered under charity number SC000278.
participants (4)
-
Brent Yorgey -
Daniel Fischer -
Jan Jakubuv -
Ken Overton