Commit e1da26c6 authored by Nicolas Lenz's avatar Nicolas Lenz ❄️
Browse files

Comparisons

parent c6e22a3b
Loading
Loading
Loading
Loading
+25 −3
Original line number Diff line number Diff line
@@ -16,15 +16,13 @@ length : List a -> Nat0
    (x::xs) => 1 + length xs
```

- DRYer

### Records

```
data Person = Person {personName :: String, personAge :: Int}  -- prefixing because of name collisions

peter :: Person
peter = Person {name = "Peter", age = 65}
peter = Person {personName = "Peter", personAge = 65}

showName :: Person -> String
showName person = "The name is " ++ name person ++ "."
@@ -42,3 +40,27 @@ peter : Person
showName : Person -> String
    person => "The name is " + person.Name + "."
```

### Traits

```
class Showable (a :: *) where
    show :: a -> String

instance Showable Person where
    show p = "The name is " ++ personName p

f :: Showable a => a -> IO ()
f x = putStrLn $ "Show: " ++ show x
```

```
trait Showable (a : Type)
    show : a -> String

Person : Showable
    show p = "The name is " + p.Name

f : (a : Showable, m : MonadTerminal) => a -> m ()
    x => print $ "Show: " + show x
```