scraps/tup.md - documents (master)

tup.md @master

cb58185

-- 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, <>>

Tree @master (Download .tar.gz)

tup.md @master