[Agda] Compile-time parsing

[Peter Thiemann]

Hi Ben,

thanks for your suggestion.
Not quite. You approach elegantly sidesteps the production of a value at 
type ⊥.
However, its result type still incorporates the choice (yes/no) between 
a correctly parsed
string and an invalid string. In contrast, I want
intLiteral "foo"
to be rejected as a type error just like
intLiteral true.

-Peter

> Hi Peter, will this sort of thing do what you want?
> - Ben
>
> On 15 December 2011 13:01, Peter Thiemann
> <thiemann at informatik.uni-freiburg.de>  wrote:
>> Hi all,
>>
>> I want to statically ensure that a string constant has a certain format.
>> That is, I want an ill-formatted constant to be a typing error.
>>
>> For example, suppose I wanted to ensure that certain string constants can be
>> parsed as integers.
>> Then there should be a function like this
>>
>> intLiteral : String ->  ParsedIntLiteral
>>
>> such that
>>
>> intLiteral "42"
>>
>> is accepted, but
>>
>> intLiteral "foo"
>>
>> is a type error.
>>
>> I made a few attempts, but did not find a satisfactory solution, yet.
>> Here is one:
>> ----------------
>>
>> isTrue : Bool → Set
>> isTrue true = ⊤
>> isTrue false = ⊥
>>
>> record Parsed (p : String → Bool) : Set where
>>   field
>>     s : String
>>     yes : isTrue (p s)
>>
>> intLiteral : (s : String) → {p : isTrue (isIntLiteral s)} → Parsed
>> isIntLiteral
>> intLiteral s {yes} = record { s = s; yes = p }
>>
>> i0 = intLiteral "0" -- ok
>> ix = intLiteral "x" -- marked yellow because the implicit arg could not be
>> inferred
>>                            -- I'd like to turn this case into a type error
>> -----------------
>> Here is another
>> -----------------
>>
>> intLiteral' : (s : String) → if isIntLiteral s then Parsed isIntLiteral else
>> ⊥
>> intLiteral' s with isIntLiteral s
>> ... | true = record { s = s }
>> ... | false = ?
>>
>> -- at the ? agda knows that the expected type is ⊥, but clearly I cannot
>> produce an element here
>> -----------------
>>
>> .... and a few other variations.
>>
>> Any suggestions?
>> -Peter
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>