-- In this case, a^n corresponds to an n-tuple whose elements are of type a -- We have a typeclass

class Conv a b where conv :: a -> b

-- And types corresponding to

type Tup t = forall n : Nat. t ^ n type Var t = forall n : Nat. (forall s. Conv s t => s) ^ n

-- we also have these two built-in primitives

generalize :: Var t -> Tup t forget :: Tup t -> [t]

-- that will usually be used together

var :: Var t -> [t]

-- We could use this to create 'variadic' functions, e.g. -- a non-type-safe but C-like printf

data PFElem = PFInt Int | PFFloat Float | PFString String

instance Conv Int PFElem where conv = PFInt instance Conv Float PFElem where conv = PFFloat instance Conv String PFElem where conv = PFString

printf :: String -> Var PFElem -> IO () printf spec args = putStr . printfInterpolate . var $ args where printfInterpolate :: String -> [PFElem] -> String printfInterpolate = {- ... -}

main :: IO () main = printf "string %s and int %d\n" ("foo", 5)

-- In Latka, we will have the Var type and the var primitive as built-ins, -- and treats a^n as a subtype of Var a in all cases. Thus, we can convert a -- value like <2,3> : Nat * Nat to a value of type Var Nat, but not the other -- way around.

-- With that machinery, we can define the following as a library:

-- word instance Conv String WordPart where {- ... -} instance Conv Word WordPart where {- ... -}

wd : Var WordPart -> Word wd = {- ... -}

-- this is well-typed, because its argument is of type String * Word <: Var WordPart puts wd.<"foo", wd.<"bar", "baz">> -- this is not, because its argument is of type String * String * (Nat * Nat) -- puts wd.<"a","b",<1,2>>

-- sentence instance Conv String SentencePart where {- ... -} instance Conv Word SentencePart where {- ... -} instance Conv Sentence SentencePart where {- ... -}

se : Var SentencePart -> Sentence se = {- ... -}

-- this is well-typed, as the argument is of type -- String * Word * Sentence <: Var SentencePart puts se.<"one", wd.<"two", "three">, se.<"four", "five">>

-- &c

--this gives us type-safe variadic functions, as well as a nice mechanism for --semi-implicitly stringifying things

cat : Var String -> String cat vs = go.(var.vs) where go [] = "" go (x::xs) = x (go.xs)

{- prints "foo5<>" -} puts cat.<"foo", 5, <>>