edwinb

data FakeChar = A | B | C
  
data ValidMyString : List Char -> Type where
     VA : ValidMyString xs -> ValidMyString ('a' :: xs)
     VB : ValidMyString xs -> ValidMyString ('b' :: xs)
     VC : ValidMyString xs -> ValidMyString ('c' :: xs)
     VNil : ValidMyString []
  
implicit fromString : (x : String) -> {auto p : ValidMyString (unpack x)}
                      -> List FakeChar

edwinb

import Process

import Data.Vect

data Counter : Type -> Type where
     GetIdle : Counter Int
     Append : Vect n a -> Vect m a -> Counter $ Vect (n + m) a

data Maths : Type -> Type where
     Factorial : Nat -> Maths Nat

edwinb

  -- This segfaults, due to an erased name being used in the case
  -- block generated for the 'j'' binding
  foo : Nat -> ((Int, String) -> Nat -> IO a) -> IO a
  foo Z k = k (0, "End") Z
  foo (S j) k = foo j (\(i', s'), j' => k (i'+1, s') j')
  
  -- This doesn't segfault, since Idris treats the \j' as an ordinary binder
  -- rather than a pattern matching one.
  foo' : Nat -> ((Int, String) -> Nat -> IO a) -> IO a
  foo' Z k = k (0, "End") Z

edwinb

module Process

import System.Concurrency.Raw
import Data.List
import System

-- Process IDs are parameterised by their interface. A request of type
-- 'iface t' has a response of type 't'
abstract
data ProcID : (iface : Type -> Type) -> Type where

edwinb

import Data.Vect
  
data Ragged : List Nat -> Type -> Type where
     Nil : Ragged [] a
     (::) : Vect n a -> Ragged ns a -> Ragged (n :: ns) a
       
test_ragged : Ragged [1,3,2] String
test_ragged = [["Foo"],
               ["Bar", "Baz", "Quux"],
               ["Thurlingdrome", "Bananas"]]

edwinb

  qsort : Ord a => List a -> List a
  qsort [] = []
  qsort (x :: xs) = let (l, r) = partition (< x) xs in
                        assert_total (qsort l ++ x :: qsort r) -- assert totality otherwise it won't reduce in the type
  
  data Singleton : a -> Type where
       MkSingleton : Singleton x
  
  t_qsort : Ord a => (xs : List a) -> Singleton (qsort xs)
  t_qsort xs = MkSingleton

edwinb

module Main

import System.Concurrency.Raw

%access public

-- Process IDs are parameterised by the type of request they are willing to
-- take (req, which is implicit), and a function which calculates the type of
-- response they'll send
abstract

edwinb

What is the appeal of dynamically-typed languages?

Kris Nuttycombe asks:

I genuinely wish I understood the appeal of unityped languages better. Can someone who really knows both well-typed and unityped explain?

I think the terms well-typed and unityped are a bit of question-begging here (you might as well say good-typed versus bad-typed), so instead I will say statically-typed and dynamically-typed.

I'm going to approach this article using Scala to stand-in for static typing and Python for dynamic typing. I feel like I am credibly proficient both languages: I don't currently write a lot of Python, but I still have affection for the language, and have probably written hundreds of thousands of lines of Python code over the years.

edwinb

AnyST : Type -> Type -> Type
AnyST s a = {m : _} -> Monad m => StateT s m a
  
foo : AnyST Integer ()
foo = do x <- get
         put (x + 1)
  
wibble : StateT Integer Maybe ()
wibble = foo
  

edwinb

-- Version 1, no possible failure

  openDoor : { [DOOR Closed] ==> [DOOR Open] } Eff ()
  openDoor = call OpenDoor
  
  closeDoor : { [DOOR Open] ==> [DOOR Closed] } Eff ()
  closeDoor = call CloseDoor
  
  knock : { [DOOR Closed] } Eff ()
  knock = call Knock