A tiny language, a subset of Haskell aimed at aiding teachers teach Haskell
Go to file
2017-06-12 17:42:08 +01:00
app Fix dictionary passing during stepper 2017-06-12 17:42:08 +01:00
examples Start of state monad 2017-06-12 11:05:53 +01:00
logo Logos 2017-05-15 14:53:52 +01:00
src Fix dictionary passing during stepper 2017-06-12 17:42:08 +01:00
static Gamma 2017-05-02 12:32:03 +01:00
web Sorted the whole problem 2017-05-07 00:58:53 +01:00
.gitignore Stackify; builds on LTS-8.9 (GHC 8.0.2) 2017-04-11 09:37:49 +01:00
build.sh Add ghcjs to build 2017-04-27 15:38:27 +01:00
duet.cabal Better error messages 2017-06-02 19:02:47 +01:00
LICENSE.md Rewrite README 2017-04-19 10:16:50 +01:00
README.md Remove forall 2017-06-07 11:37:26 +01:00
stack-ghcjs.yaml Add ghcjs to build 2017-04-27 15:38:27 +01:00
stack.yaml Now all names are supplied uniquely, just need to implement renamer 2017-04-26 19:55:38 +01:00
TODO.org Move to examples/ 2017-05-08 11:44:52 +02:00

Duet

A programming language focused on interactive collaboration between the developer and the computer.

Web releases

Command-line usage

Run with the file and function to evaluate:

$ stack exec duet File.hs main

Output looks like:

$ stack exec duet examples/X.hs main
-- Type checking ...
Just :: forall g0. g0 -> Maybe g0
Nothing :: forall g0. Maybe g0
Left :: forall g0 g1. g0 -> Either g0 g1
Right :: forall g0 g1. g1 -> Either g0 g1
X :: Either (Maybe Bool) Bool -> X
Y :: Y
-- Source:
compose = (\f g x -> ((f :: g4 -> g5) (((g :: g3 -> g4) (x :: g3) :: g4)) :: g5) :: (g4 -> g5) -> (g3 -> g4) -> g3 -> g5)
id = (\x -> (x :: g7) :: g7 -> g7)
and = (\x y -> (if (x :: Bool) then (if (y :: Bool) then (True :: Bool) else (False :: Bool) :: Bool) else (False :: Bool) :: Bool) :: Bool -> Bool -> Bool)
main = ((Just :: String -> Maybe String) ((if (True :: Bool) then ("ok!" :: String) else ("nope" :: String) :: String)) :: Maybe String)
-- Stepping ...
Just (if True then "ok!" else "nope")
Just "ok!"

Looks like

The below is a pretty comprehensive example of supported syntax so far:

data List a = Nil | Cons a (List a)
data Tuple a b = Tuple a b
class Functor (f :: Type -> Type) where
  map :: (a -> b) -> f a -> f b
instance Functor Maybe where
  map = \f m ->
    case m of
      Nothing -> Nothing
      Just a -> Just (f a)
data Maybe a = Nothing | Just a
id = \x -> x
not = \p -> if p then False else True
foldr = \cons nil l ->
  case l of
    Nil -> nil
    Cons x xs -> cons x (foldr cons nil xs)
foldl = \f z l ->
  case l of
    Nil -> z
    Cons x xs -> foldl f (f z x) xs
map = \f xs ->
  case xs of
    Nil -> Nil
    Cons x xs -> Cons (f x) (map f xs)
zip = \xs ys ->
  case Tuple xs ys of
    Tuple Nil _ -> Nil
    Tuple _ Nil -> Nil
    Tuple (Cons x xs1) (Cons y ys1) ->
      Cons (Tuple x y) (zip xs1 ys1)
list = (Cons True (Cons False Nil))
main = zip list (map not list)

Holes

Anything prefixed with _ is a hole of any type. The substitutor does not try to expand it. This is useful for seeing how code evaluates for any f or writing proofs:

data List a = Nil | Cons a (List a)
foldr = \f z l ->
  case l of
    Nil -> z
    Cons x xs -> f x (foldr f z xs)
foldl = \f z l ->
  case l of
    Nil -> z
    Cons x xs -> foldl f (f z x) xs
list = (Cons True (Cons False Nil))
> main = foldr _f _nil list
foldr _f _nil list
_f True (foldr _f _nil (Cons False Nil))
_f True (_f False (foldr _f _nil Nil))
_f True (_f False _nil)
> main = foldl _f _nil list
foldl _f _nil list
foldl _f (_f _nil True) (Cons False Nil)
foldl _f (_f (_f _nil True) False) Nil
_f (_f _nil True) False

Type-classes

Type-classes are supported, as in this example:

data Maybe a = Nothing | Just a
class Functor (f :: Type -> Type) where
  map :: forall a b. (a -> b) -> f a -> f b
instance Functor Maybe where
  map = \f m ->
    case m of
      Nothing -> Nothing
      Just a -> Just (f a)
not = \b -> case b of
              True -> False
              False -> True
main = map not (Just True)

Kind inference is not implemented, so if you want a kind other than Type (aka * in Haskell), you have to put a kind signature on the type variable.