ad hoc user-defined types

[sfultong]

What is the minimal features we need to add to Telomare to allow for ad hoc user-defined types?

The way I see user-defined types, is that they're nominal typing on top of structural typing. Or rather, they're simply unique labels on top of structure definitions. Since Telomare already is capable of defining arbitrary structures in a sort of untyped way, all we need to add is support of unique labels.

By labels, I really mean natural numbers, since they're isomorphically equivalent.

So, if we add a keyword to Telomare called "unique", then we can define top-level functions:
MyInt = unique
This will assign a unique natural number to MyInt at compile time.

Then we can use this tag later on, in smart constructors:
toMyint = \i -> if i < 1 or i > 9 then abort "MyInts must be between 1 and 9 inclusive" else (MyInt, i)

and check against this tag identifier for "type checking":
incrementMyInt = \i -> let checkedI = if left l == MyInt then right i else abort "incrementMyInt: expecting a MyInt" in toMyInt (succ checkedi)

This is obviously a bit messy and could use more syntatic sugar, but it should demonstrate the basic concept

[sfultong]

I forgot to mention:

One thing to be mindful about with the design of unique is serialization. If we want to serialize "typed" data, that data should be dependent on the code that generated it. Thus, unique should probably be some deterministic hash of the parsed grammar.

[sfultong]

We can combine a smart constructor and the type checking function in one:

MyInt = let intTag = unique in (\i -> if i < 1 or i > 9 then abort "MyInts must be between 1 and 9 inclusive" else (intTag, i), \i -> if left i == intTag then 0 else "expecting MyInt")

Let's assume we change : to mean \x c -> let testResult = c x in if testResult then abort testResult else x

Then we can have a type signature like:
incrementMyInt = \i : (right MyInt) -> ...

Note that i changed the location of the colon from the first post in this issue. right MyInt is a little ugly, but ... again, I'm fine with ugliness now, and later we might think of good syntactic sugar.

[sfultong]

Here's an alternative to unique: have an operator that returns the hash of the AST of an expression.

Then we can do

MyInt = let wrapper = \h -> (\i -> if i < 1 or i > 9 then abort "MyInts must be between 1 and 9 inclusive" else (h, i), \i -> if left i == h then 0 else "expecting MyInt")
        in wrapper (# wrapper)

[sfultong]

This way custom data types are stable until the code defining them is changed

[hhefesto]

MyInt = let wrapper = \h -> ( \i -> if i < 1 or i > 9
                                    then abort "MyInts must be between 1 and 9 exclusive"
                                    else (h, i)
                            , \i -> if left i == h
                                    then 0
                                    else "expecting MyInt"
                            )
        in wrapper (# wrapper)

[sfultong]

#71 could unlock some interesting possibilities for this. I'm wondering if : could mean "reverse function". Then checking a type would simply be a matter of seeing if a reversed smart constructor could be applied to an argument, and we wouldn't have to have the second part of the pair under wrapper

[hhefesto]

MyInt = let wrapper = \h -> ( \i -> if not i
                                    then "MyInt must not be 0"
                                    else  i
                            , \i -> if dEqual (left i)
                                    then 0
                                    else "expecting MyInt"
                            )
        in wrapper (# wrapper)
main = \i -> ((right MyInt) 8, 0)

This runs without complaining:

[hhefesto@olimpo:~/src/telomare]$ cabal run telomare examples.tel
Up to date

done

Why? 🧐🤔

[sfultong]

There isn't any abort There. Right now, the only place that an abort check happens is with the : operator

[hhefesto]

What is weirdest for me is that ((right MyInt) 8, 0) runs , \i -> if dEqual (left i) and dEqual still needs another argument, but it doesn't fail.

[hhefesto]

Leaving this here for safe keeping (from gitter):

sfultong
@sfultong
Jul 16 13:42
didn't we have a discussion at one point about having parseRefinementCheck in parseLambda?
Daniel Herrera Rendón
@hhefesto
Jul 16 13:42
I think so
sfultong
@sfultong
Jul 16 13:42
I think maybe we decided it wasn't worth it because parseLambda might have multiple lambda variables, and that would be complicated with :
but it would be convenient syntactic sugar
then we could do

\i : (\i -> assert i "MyInt must not be 0") -> (h, i)

the two i lambdas is awkward though, so the design of : probably needs tweaking
sfultong
@sfultong
Jul 16 13:51
it would be nicest if we could do

\i : assert i "MyInt must not be 0" -> (h, i)

[hhefesto]

There isn't any abort There. Right now, the only place that an abort check happens is with the : operator

I'm trying to do a small abort with the current syntax.

I'm still not too aware of how : currently works, but from parseRefinementCheck :: TelomareParser (UnprocessedParsedTerm -> UnprocessedParsedTerm) I came up with:

main : (4,3) 0 = \input -> ("Hello, World!", 0)

but that breaks with:

[hhefesto@olimpo:~/src/telomare]$ cabal run telomare examples.tel
Up to date
telomare: src/Telomare/Possible.hs:(124,23)-(143,39): Non-exhaustive patterns in case

I didn't go any deeper.
@sfultong : Should I go deeper or are you aware of an easy way to trigger an abort?

[sfultong]

Hmm, I should probably look into why Possible is failing there. That's not exactly how the : operator should be used, but it should fail more gracefully.

Look at the refinement section in Spec.hs for better examples

[hhefesto]

Thanks!

For completeness:

-- refinement fail example:2
main : (\x -> if x then "fail" else 0) = 1

fails with: compilation failed somehow, with result Left (StaticCheckError "fail")

[hhefesto]

how about this syntax:

MyInt = let wrapper = \h -> ( \i -> if not i
                                    then abort "MyInt cannot be 0"
                                    else  (h, i)
                            , \i -> if dEqual (left i) h
                                    then 0 -- TODO: Ask sam is this should be 1 instead
                                    else abort "Not a MyInt"
                            )
        in wrapper (# wrapper)

increaseMyInt : (right MyInt) = \ (x : (right MyInt))  -> (left MyInt) (succ (right x))

main = \i -> (increaseMyInt ((left MyInt) 8), 0)

n.b. MyInt constructor returns a tuple with the hash and the data of MyInt

n.b.2. \x : foo -> bar syntax has to be implemented

thoughts? @sfultong

[sfultong]

Yeah, I intended that the : operator be available in lambda bindings as well as let bindings, so this looks good