diff --git a/src/main.rs b/src/main.rs
index 93b247e..80e93df 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -14,7 +14,15 @@ mod types;
 use diagnostics::render;
 use interpreter::Interpreter;
 use parser::Parser;
-use std::io::{self, Write};
+use rustyline::completion::{Completer, Pair};
+use rustyline::error::ReadlineError;
+use rustyline::highlight::Highlighter;
+use rustyline::hint::Hinter;
+use rustyline::history::DefaultHistory;
+use rustyline::validate::Validator;
+use rustyline::{Config, Editor, Helper};
+use std::borrow::Cow;
+use std::collections::HashSet;
 use typechecker::TypeChecker;
 
 const VERSION: &str = "0.1.0";
@@ -26,28 +34,33 @@ Commands:
   :help, :h       Show this help
   :quit, :q       Exit the REPL
   :type <expr>    Show the type of an expression
+  :info <name>    Show info about a binding
+  :env            Show user-defined bindings
   :clear          Clear the environment
   :load <file>    Load and execute a file
   :trace on/off   Enable/disable effect tracing
   :traces         Show recorded effect traces
 
+Keyboard:
+  Tab             Autocomplete
+  Ctrl-C          Cancel current input
+  Ctrl-D          Exit
+  Up/Down         Browse history
+  Ctrl-R          Search history
+
 Examples:
   > let x = 42
   > x + 1
   43
 
   > fn double(n: Int): Int = n * 2
+  > :type double
+  double : fn(Int) -> Int
   > double(21)
   42
 
-  > Console.print("Hello, world!")
-  Hello, world!
-
-Debugging:
-  > :trace on
-  > Console.print("test")
-  > :traces
-  [   0.123ms] Console.print("test") → ()
+  > match Some(5) { Some(x) => x, None => 0 }
+  5
 "#;
 
 fn main() {
@@ -114,69 +127,255 @@ fn run_file(path: &str) {
     }
 }
 
+/// REPL helper for tab completion and syntax highlighting
+struct LuxHelper {
+    keywords: HashSet<String>,
+    commands: Vec<String>,
+    user_defined: HashSet<String>,
+}
+
+impl LuxHelper {
+    fn new() -> Self {
+        let keywords: HashSet<String> = vec![
+            "fn", "let", "if", "then", "else", "match", "with", "effect", "handler",
+            "handle", "resume", "type", "import", "pub", "is", "pure", "total",
+            "idempotent", "deterministic", "commutative", "where", "assume", "true",
+            "false", "None", "Some", "Ok", "Err", "Int", "Float", "String", "Bool",
+            "Char", "Unit", "Option", "Result", "List",
+        ]
+        .into_iter()
+        .map(String::from)
+        .collect();
+
+        let commands = vec![
+            ":help", ":h", ":quit", ":q", ":type", ":t", ":clear", ":load", ":l",
+            ":trace", ":traces", ":info", ":i", ":env",
+        ]
+        .into_iter()
+        .map(String::from)
+        .collect();
+
+        Self {
+            keywords,
+            commands,
+            user_defined: HashSet::new(),
+        }
+    }
+
+    fn add_definition(&mut self, name: &str) {
+        self.user_defined.insert(name.to_string());
+    }
+}
+
+impl Completer for LuxHelper {
+    type Candidate = Pair;
+
+    fn complete(
+        &self,
+        line: &str,
+        pos: usize,
+        _ctx: &rustyline::Context<'_>,
+    ) -> rustyline::Result<(usize, Vec<Pair>)> {
+        // Find the start of the current word
+        let start = line[..pos]
+            .rfind(|c: char| c.is_whitespace() || "(){}[],.;:".contains(c))
+            .map(|i| i + 1)
+            .unwrap_or(0);
+
+        let prefix = &line[start..pos];
+
+        if prefix.is_empty() {
+            return Ok((pos, Vec::new()));
+        }
+
+        let mut completions = Vec::new();
+
+        // Complete commands
+        if prefix.starts_with(':') {
+            for cmd in &self.commands {
+                if cmd.starts_with(prefix) {
+                    completions.push(Pair {
+                        display: cmd.clone(),
+                        replacement: cmd.clone(),
+                    });
+                }
+            }
+        } else {
+            // Complete keywords
+            for kw in &self.keywords {
+                if kw.starts_with(prefix) {
+                    completions.push(Pair {
+                        display: kw.clone(),
+                        replacement: kw.clone(),
+                    });
+                }
+            }
+            // Complete user-defined names
+            for name in &self.user_defined {
+                if name.starts_with(prefix) {
+                    completions.push(Pair {
+                        display: name.clone(),
+                        replacement: name.clone(),
+                    });
+                }
+            }
+        }
+
+        Ok((start, completions))
+    }
+}
+
+impl Hinter for LuxHelper {
+    type Hint = String;
+
+    fn hint(&self, _line: &str, _pos: usize, _ctx: &rustyline::Context<'_>) -> Option<String> {
+        None
+    }
+}
+
+impl Highlighter for LuxHelper {
+    fn highlight_hint<'h>(&self, hint: &'h str) -> Cow<'h, str> {
+        Cow::Owned(format!("\x1b[90m{}\x1b[0m", hint))
+    }
+}
+
+impl Validator for LuxHelper {}
+impl Helper for LuxHelper {}
+
+fn get_history_path() -> Option<std::path::PathBuf> {
+    std::env::var_os("HOME").map(|home| {
+        std::path::PathBuf::from(home).join(".lux_history")
+    })
+}
+
 fn run_repl() {
     println!("Lux v{}", VERSION);
     println!("Type :help for help, :quit to exit\n");
 
+    let config = Config::builder()
+        .history_ignore_space(true)
+        .completion_type(rustyline::CompletionType::List)
+        .edit_mode(rustyline::EditMode::Emacs)
+        .build();
+
+    let helper = LuxHelper::new();
+    let mut rl: Editor<LuxHelper, DefaultHistory> = Editor::with_config(config).unwrap();
+    rl.set_helper(Some(helper));
+
+    // Load history
+    if let Some(history_path) = get_history_path() {
+        if let Some(parent) = history_path.parent() {
+            let _ = std::fs::create_dir_all(parent);
+        }
+        let _ = rl.load_history(&history_path);
+    }
+
     let mut interp = Interpreter::new();
     let mut checker = TypeChecker::new();
     let mut buffer = String::new();
     let mut continuation = false;
 
     loop {
-        // Print prompt
         let prompt = if continuation { "... " } else { "lux> " };
-        print!("{}", prompt);
-        io::stdout().flush().unwrap();
 
-        // Read input
-        let mut line = String::new();
-        match io::stdin().read_line(&mut line) {
-            Ok(0) => break, // EOF
-            Ok(_) => {}
-            Err(e) => {
-                eprintln!("Error reading input: {}", e);
-                continue;
+        match rl.readline(prompt) {
+            Ok(line) => {
+                let line = line.trim_end().to_string();
+
+                // Don't add empty lines or continuations to history
+                if !line.is_empty() && !continuation {
+                    let _ = rl.add_history_entry(line.as_str());
+                }
+
+                // Handle commands
+                if !continuation && line.starts_with(':') {
+                    handle_command(&line, &mut interp, &mut checker, rl.helper_mut().unwrap());
+                    continue;
+                }
+
+                // Accumulate input
+                buffer.push_str(&line);
+                buffer.push('\n');
+
+                // Check for continuation (unbalanced braces/parens)
+                let open_braces = buffer.chars().filter(|c| *c == '{').count();
+                let close_braces = buffer.chars().filter(|c| *c == '}').count();
+                let open_parens = buffer.chars().filter(|c| *c == '(').count();
+                let close_parens = buffer.chars().filter(|c| *c == ')').count();
+
+                if open_braces > close_braces || open_parens > close_parens {
+                    continuation = true;
+                    continue;
+                }
+
+                continuation = false;
+                let input = std::mem::take(&mut buffer);
+
+                if input.trim().is_empty() {
+                    continue;
+                }
+
+                // Track new definitions for completion
+                if let Some(name) = extract_definition_name(&input) {
+                    rl.helper_mut().unwrap().add_definition(&name);
+                }
+
+                eval_input(&input, &mut interp, &mut checker);
+            }
+            Err(ReadlineError::Interrupted) => {
+                // Ctrl-C: clear buffer
+                buffer.clear();
+                continuation = false;
+                println!("^C");
+            }
+            Err(ReadlineError::Eof) => {
+                // Ctrl-D: exit
+                break;
+            }
+            Err(err) => {
+                eprintln!("Error: {:?}", err);
+                break;
             }
         }
+    }
 
-        let line = line.trim_end();
-
-        // Handle commands
-        if !continuation && line.starts_with(':') {
-            handle_command(line, &mut interp, &mut checker);
-            continue;
-        }
-
-        // Accumulate input
-        buffer.push_str(line);
-        buffer.push('\n');
-
-        // Check for continuation (simple heuristic: unbalanced braces)
-        let open_braces = buffer.chars().filter(|c| *c == '{').count();
-        let close_braces = buffer.chars().filter(|c| *c == '}').count();
-        let open_parens = buffer.chars().filter(|c| *c == '(').count();
-        let close_parens = buffer.chars().filter(|c| *c == ')').count();
-
-        if open_braces > close_braces || open_parens > close_parens {
-            continuation = true;
-            continue;
-        }
-
-        continuation = false;
-        let input = std::mem::take(&mut buffer);
-
-        if input.trim().is_empty() {
-            continue;
-        }
-
-        eval_input(&input, &mut interp, &mut checker);
+    // Save history
+    if let Some(history_path) = get_history_path() {
+        let _ = rl.save_history(&history_path);
     }
 
     println!("\nGoodbye!");
 }
 
-fn handle_command(line: &str, interp: &mut Interpreter, checker: &mut TypeChecker) {
+fn extract_definition_name(input: &str) -> Option<String> {
+    let input = input.trim();
+    if input.starts_with("fn ") {
+        input.split_whitespace().nth(1).and_then(|s| {
+            s.split('(').next().map(String::from)
+        })
+    } else if input.starts_with("let ") {
+        input.split_whitespace().nth(1).and_then(|s| {
+            s.split([':', '=']).next().map(|s| s.trim().to_string())
+        })
+    } else if input.starts_with("type ") {
+        input.split_whitespace().nth(1).and_then(|s| {
+            s.split(['<', '=']).next().map(|s| s.trim().to_string())
+        })
+    } else if input.starts_with("effect ") {
+        input.split_whitespace().nth(1).map(|s| {
+            s.trim_end_matches('{').trim().to_string()
+        })
+    } else {
+        None
+    }
+}
+
+fn handle_command(
+    line: &str,
+    interp: &mut Interpreter,
+    checker: &mut TypeChecker,
+    helper: &mut LuxHelper,
+) {
     let parts: Vec<&str> = line.splitn(2, ' ').collect();
     let cmd = parts[0];
     let arg = parts.get(1).map(|s| s.trim());
@@ -196,14 +395,25 @@ fn handle_command(line: &str, interp: &mut Interpreter, checker: &mut TypeChecke
                 println!("Usage: :type <expression>");
             }
         }
+        ":info" | ":i" => {
+            if let Some(name) = arg {
+                show_info(name, checker);
+            } else {
+                println!("Usage: :info <name>");
+            }
+        }
+        ":env" => {
+            show_environment(checker, helper);
+        }
         ":clear" => {
             *interp = Interpreter::new();
             *checker = TypeChecker::new();
+            helper.user_defined.clear();
             println!("Environment cleared.");
         }
         ":load" | ":l" => {
             if let Some(path) = arg {
-                load_file(path, interp, checker);
+                load_file(path, interp, checker, helper);
             } else {
                 println!("Usage: :load <filename>");
             }
@@ -235,6 +445,30 @@ fn handle_command(line: &str, interp: &mut Interpreter, checker: &mut TypeChecke
     }
 }
 
+fn show_info(name: &str, checker: &TypeChecker) {
+    // Look up in the type environment
+    if let Some(scheme) = checker.lookup(name) {
+        println!("{} : {}", name, scheme);
+    } else {
+        println!("'{}' is not defined.", name);
+    }
+}
+
+fn show_environment(checker: &TypeChecker, helper: &LuxHelper) {
+    println!("User-defined bindings:");
+    if helper.user_defined.is_empty() {
+        println!("  (none)");
+    } else {
+        for name in &helper.user_defined {
+            if let Some(scheme) = checker.lookup(name) {
+                println!("  {} : {}", name, scheme);
+            } else {
+                println!("  {} : <unknown>", name);
+            }
+        }
+    }
+}
+
 fn show_type(expr_str: &str, checker: &mut TypeChecker) {
     // Wrap expression in a let to parse it
     let wrapped = format!("let _expr_ = {}", expr_str);
@@ -255,7 +489,7 @@ fn show_type(expr_str: &str, checker: &mut TypeChecker) {
     }
 }
 
-fn load_file(path: &str, interp: &mut Interpreter, checker: &mut TypeChecker) {
+fn load_file(path: &str, interp: &mut Interpreter, checker: &mut TypeChecker, helper: &mut LuxHelper) {
     let source = match std::fs::read_to_string(path) {
         Ok(s) => s,
         Err(e) => {
@@ -279,6 +513,13 @@ fn load_file(path: &str, interp: &mut Interpreter, checker: &mut TypeChecker) {
         return;
     }
 
+    // Add definitions for completion
+    for decl in &program.declarations {
+        if let Some(name) = extract_definition_name(&format!("{:?}", decl)) {
+            helper.add_definition(&name);
+        }
+    }
+
     match interp.run(&program) {
         Ok(_) => println!("Loaded '{}'", path),
         Err(e) => println!("Runtime error: {}", e),
diff --git a/src/typechecker.rs b/src/typechecker.rs
index e0d3d5b..9c11769 100644
--- a/src/typechecker.rs
+++ b/src/typechecker.rs
@@ -114,6 +114,11 @@ impl TypeChecker {
         }
     }
 
+    /// Look up a type scheme by name (for REPL :info command)
+    pub fn lookup(&self, name: &str) -> Option<&TypeScheme> {
+        self.env.bindings.get(name)
+    }
+
     /// Type check a program
     pub fn check_program(&mut self, program: &Program) -> Result<(), Vec<TypeError>> {
         // First pass: collect all declarations