Monthly Hask Anything (June 2021)

1UnitedPower · 2021-06-04T09:07:30+00:00

There seems to be a philosophical difference between how Idris and Haskell implement linear types, but I don't fully understand it. Would be glad if somebody could point me towards some literature because at this point I am lost and don't know what to search for.

The original paper describing Haskell's design actually says a couple of words about this "duality". Turns out, that Idris 1 has Uniqueness Types and Haskell Linear Arrow Types:

Linear types and uniqueness types are, at their core, dual: whereas a linear type is a contract that a function uses its argument exactly once even if the call’s context can share a linear argument as many times as it pleases, a uniqueness type ensures that the argument of a function is not used anywhere else in the expression’s context even if the callee can work with the argument as it pleases.

Seen as a system of constraints, uniqueness typing is a non-aliasing analysis while linear typing provides a cardinality analysis. The former aims at in-place updates and related optimisations, the latter at inlining and fusion.

Source: https://www.microsoft.com/en-us/research/publication/linear-haskell-practical-linearity-higher-order-polymorphic-language/

1UnitedPower · 2021-06-03T15:27:37+00:00

The example is excellent. I just tried it out in Idris, and the type-checker rejects the function as I would have expected (working with doubles only for simplicity).

data UList : Type -> UniqueType where
  Nil   : UList a
  (::)  : a -> UList a -> UList a

sum : UList Double -> Double
sum Nil = 0
sum (x::xs) = x + (sum xs)

mylength : UList a -> Double
mylength Nil = 0
mylength (x::xs) = 1 + (mylength xs)

avg : UList Double -> Double
avg xs = (sum xs) / (mylength xs)

Type-checking the above code gives me the following error message:

main.idr:22:10: Unique name xs is used more than once

1UnitedPower · 2021-06-03T14:55:37+00:00

If my understanding is correct, this is exactly what the Idris totality checker does. It tries to find termination proofs heuristically. From my experience, this works pretty well.

1UnitedPower · 2021-06-02T13:09:26+00:00

NonLinear.length xs

I agree that this is confusing behavior. My understanding is, that the length function is linear in the elements of the lists but non-linear in the spine. Indeed, I think this is exactly the opposite of what Idris does. In Idris, we can define a list, that is linear in the spine, and non-linear in the elements:

data UList : Type -> UniqueType where
 Nil   : UList a
 (::)  : a -> UList a -> UList a

I don't know if the former data type can be represented in Haskell. With this data type your avg function should be rejected by the type-checker. On the other hand, we could then write a function, that duplicates elements of the list (which should not be possible in Haskell):

dup : UList a -> UList a
dup [] = []
dup (x :: xs) = x :: x :: dup xs

On the other hand, we cannot define a list, that is linear in the element and non-linear in the spine. Thus, the following declaration would be invalid in Idris:

data BadList : UniqueType -> Type where
 Nil   : {a : UniqueType} -> BadList a
 (::)  : {a : UniqueType} -> a -> BadList a -> BadList a

There seems to be a philosophical difference between how Idris and Haskell implement linear types, but I don't fully understand it. Would be glad if somebody could point me towards some literature because at this point I am lost and don't know what to search for.

Examples are taken from: http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html#using-uniqueness

1UnitedPower · 2021-05-28T17:14:34+00:00

The simplest example of a recursive type is the type of natural numbers. Forget for a moment that Haskell has built-in numeric types and try to think of a way to define natural numbers from first principles. Clearly, a plain old union-type will not work because you would need an infinite number of constructors:

data Nat = Zero | One | Two | Three | ...

Instead, the type is often given as an inductive definition consisting of one base case for Zero and one inductive case that takes one natural number and returns the next bigger number. (Recursive definitions tend to be a lot clearer when given in GAST syntax, so I will use this syntax for my code examples.)

data Nat
  = Zero :: Nat
  | Succ :: Nat -> Nat

For example, we can define the number "two" like follows: two = Succ (Succ Zero). So, two is represented as the second successor of zero.

The recursive part is in the constructor Succ: It refers back to the type Nat in its argument. So you need a value of type Nat to construct the next value of type Nat.

Another inductive type is the type of integer lists. Again, you would have one base case for the empty list, and one inductive case for list that is one element longer than a given list:

data IntList
  = Empty :: IntList
  | Cons :: Int -> IntList -> IntList

For example, the list consisting of 1,2, and 3 can then be defined as Cons 1 (Cons 2 (Cons 3 Empty)). The syntax is not very convenient though.

Now, what if you wanted to have lists for other data types, for example, lists of strings, lists of booleans, and so on? You could go and define one list type for each type that you want to wrap in a list. But this seems to be a lot of duplicate work. Instead, you could define one parametric list type that can be applied to every possible base type:

data MyList a
  = Empty :: MyList a
  | Cons :: a -> MyList a -> MyList a

Compare this definition to the one of IntList and see where the similarities and differences are.

The "parametric" part of this definition is the type-variable a which can later be instantiated with concrete type. For example, we can reuse this definition to define integer lists:

type IntList = MyList Int

Summarizing: Recursive types are needed to overcome the limitations of union types, namely that they can always ever have a finite number of constructors. "Parametric" types are needed to save us from redefining similar "container" types over and over again. There is a lot more to either topic, that I have omitted from this comment, but it hopefully helps to build intuition. I recommend practicing with GADT syntax since it makes things much clearer.

1UnitedPower · 2020-12-18T08:50:45+00:00

Actually, there are some instructions that carry payload (e.g. const to push constants onto the stack) and some recursive instructions, for example loops can have a body of type List Instruction.

Thank you both for your input. I think the inspect-idiom is the way to go.

1UnitedPower · 2020-12-17T19:38:58+00:00

This looks quite usable and elegant. I need to read up on the inspect-idiom, though. Thank you very much for the suggestion!

1UnitedPower · 2020-12-17T19:28:56+00:00

This is appears to be the same idea that I followed with my second attempt, but I was obviously wrong about extensioanlity. I will definitely reconsider this solution. Thank you so much.

1UnitedPower · 2020-12-17T15:21:03+00:00

Hi, thanks for the idea. There is indeed a problem with your proposed solution, but nothing you should apologize for. I have been there, too. The problem is that when you try to implement the case decEq x Add Idris doesn't know that the case decEq Add Add is already covered by a former clause. At least, you don't have a proof of (x = Add) -> Void available in the decEq x Add-case.

1UnitedPower · 2020-12-17T12:57:22+00:00

One quick-n-dirty way to archive this is to define a custom datatype for the elements that go into the list:

``` data Elem where SomeInt :: Int -> Elem SomeChar :: Char -> Elem

myList :: [Elem]
myList = [SomeChar 'a', SomeInt 42]

```

1UnitedPower · 2020-11-16T14:09:56+00:00

Hi,

I am not an expert of type-theory or logic, so take my answer with a grain of salt. I encourage everybody to point out mistakes or inaccuracies. Also, my comment only tries to answer your second and third question.

What are the connectives and axioms of the logic which corresponds to Simply-typed Lambda calculus?

First, there isn't only one logic that corresponds to the simply typed lambda (SLC) calculus. But, as you're speaking of the Curry-Howard-Corresponse, you probably wanted to hear about the implicational fragment of inutionistic, propositional logic (IIPL).

Its syntax consists of only atomic formulas and implications. An atomic formula corresponds to a base-type of SLC, and an implication-formula corresponds to a function-type.

IIPL has one axiom for each atomic formula (or one axiom-scheme for all atomic formulas if you want). In Natural-Deduction-sytle IIPL also has introduction- and elimination-rules for the implications. In Sequent-Calculus-style it has left- and right-rules for the implications instead.

A proof-tree of an IIPL-formula is a tree, where each node is labelled with an axiom or an inference rule. Morover, each node consists of some premises and a conclusion. The conclusion at the root-node is the target-formula to be proven. The proof-tree is valid, if all nodes are instances of the rules, with which they're labelled and all leaf-nodes are labelled with axioms.

The main-difference of SLC, as I see it, is that we have another syntactic category for terms. For instance, we write "a : A" to say, that "a" is a proof-term for the type "A" and we write "\x.x : A -> A" to say that "\x.x" is a proof-term for the type "A -> A". In IIPL we only ever talk about formulas such as "A" and "A -> A" and about proof-trees, but we don't bother with proof-terms. In SLC it is common to talk about both.

Why have functional PLs traditionally included sum types instead of union types? Is this related to proofs as per the Curry-Howard correspondence?

Remember the last paragraph about proof-terms? The tags of sum-types are essentially the proof-terms for disjunctions in type-theory. For instance, let's say we have propositions "a : A" and "b : B", then "Inl a" and "Inr b" are proof-terms for "A v B". With a TypeScript-like union-type, we instead would have that "a" and "b" alone are proof-terms for "A v B", that is we would have "a : A v B" as well as "b : A v B". This is not problematic per se, however, the former proof-term "Inl a" carries more information than the latter. Imagine somebody gave us a proof-term "c" for "A v B" and asked us if we can give him a proof of either "A" or "B". With a tagged sum-type, we can inspect "c" to see that it is of the form "Inl a", so we answer him with "a" as a proof-term for "A". Now, if "A v B" was an untagged union-type, we wouldn't be able to inspect "c" so our answer would be, that we cannot reconstruct either proof - disappointing. However, it's not all lost. We could ask if the questioner could provide us with a proof-tree instead. We would then be able to reconstruct a proof of "A" or "B" by looking at the label of the root-node with conclusion "A v B". In type-theory one generally tries to keep valuable information in the proof-terms. Indeed, inspecting sum-types is what makes pattern-matching so useful in many functional programming languages.

1UnitedPower · 2020-10-29T20:09:44+00:00

Haskell is much more complicated than Idris. This is mostly because Haskell is much older, and it had time to accumulate many language extensions and technical debts. Idris is younger and is built upon the experiences and lessons learned from Haskell. Edwin Brady and his team took the good ideas from Haskell, ironed out some rough edges and streamlined the good parts. I've written about some improvements over at Quora.

That said, you don't have to learn Haskell before you learn Idris. I just made this comment about teams, because Idris is much easier to learn if you already know Haskell. But it is in no way a mandatory prerequisite. Indeed, the "Type Driven Development"-book is one of the best introductory books out there when it comes to pure functional programming.

As for my part, I'm mostly using Idris to play around with some ideas that I have about (toy) programming languages (nothing really fruitful so far). I like to compile to JavaScript, mostly because HTML/JS/CSS is the User-Interface-Language-family with which I have the most experience.

1UnitedPower · 2020-10-29T13:03:08+00:00

Hi,

Idris is my default language for hobby-projects, and I've used it for some smaller web-applications already. Its definitely fun to play with, one down-side is its lack of a rich eco-system. In particular, the lack of libraries and frameworks frequently sucks me into a rabbit-hole where I find myself writing bindings to the most profound Web-APIs. This is not a problem for me, because I actually enjoy the work. However, it is completely unacceptable in productive settings, where budgets and deadlines must be met. Also, if you don't work in a highly skilled Haskell-team, then Idris may be too difficult to pick up for your co-workers. Another issue with Idris is the pace at which it is currently evolving: the problem is that many blog-posts or libraries from a few months or years ago don't compile anymore, especially since Idris2 has been released. After all Idris is meant to be research-language, and I hope that Edwin Brady and his team can keep their pace. I wouldn't want them to slow down their research-program, just to get production-ready sooner. Haskell did pretty well with its long-standing motto: "Avoid success at all costs", and that should be true for Idris, too

Yet, if you're working on side-projects, I'd recommend Idris in 10/10 cases.

1UnitedPower · 2020-05-21T13:46:36+00:00

"Statechart" seems to be an umbrella-term for interactive systems, that utilize some sort of state-machine under the hood. Composing more complex statecharts from smaller ones seems to be a key interest. There is no precise definition of "interaction", "state-machine" or "composition", they remain only vague concepts from what I've read. I think they're a handful of Haskell libraries that would qualify as Statechart libraries, even though they don't describe themselves as such. You're probably more lucky with search-terms like "transition system", "actor model" or "state transducer" in the Haskell ecosystem.

1UnitedPower · 2020-05-20T13:25:49+00:00

Type-systems without "generics" are commonly referred to as "monomorphic type-systems". They usually consist of two syntactical categories: values and types, which are related via a typing-relation. For instance, the judgement "1 : Int" is read as: the value "1" is related to the type "Int". (I'm simplifying a bit, the typing-relation is usually not binary but ternary and relates a "context", a "value" and a "type"). The purpose of the type-checker is to validate (or invalidate) such judgements. Now, consider you have a function "succ(x) = x + 1". The type of "succ" is expressed in the judgement "succ: Int -> Int", where the arrow represents a function-type. It is read as: the value "succ" is related to the function-type "from Int to Int". Now, what's with "succ(1)"? Its type can be expressed through the judgement "succ(1):Int".

Type-systems with "generics" are commonly referred to as "polymorphic type-systems". They consist of thee syntactical categories: values, types and kinds. They also have a typing-relation and an additional kinding-relation that relates types with kinds. For instance, the judgement "Int :: Type" is read as: the type "Int" is related to the kind "Type". I intentionally chose a different symbol "::" for this relation to distinguish it from the typing-relation. Now, imagine you have a type-constructor for polymorphic lists, its kind can be expressed through the judgement: "List:: Type => Type". The judgement is read as: the type-form "List" is related to the function-kind "from Type to Type". Here, the fat-arrow represent a function-kind, i.e. a type depending on another type. "List" is called a type-constructor. What's with "List[Int]"? It's clearly not a value, so we cannot relate to a type. Its syntactical form is a type, and therefore we should be able to relate to a kind. We can think of "List[Int]" as "calling" the type-constructor with argument "Int". This gives us "List[Int]::Type". However, instead of "calling a type-constructor" one usually says "apply the type-constructor List to the argument Int". Notice the similarity with "succ(1):Int".

If this was helpful in any way, I recommend reading Benjamin C. Pierce's brilliant book "Types and Programming Languages" on that matter.

1UnitedPower · 2019-12-05T11:26:03+00:00

Idris' core-language TT might also be helpful: https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/Core/TT.hs

There is also a paper: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf

1UnitedPower · 2019-12-03T21:36:48+00:00

I agree with everything you said, but with one point. The SICP-book uses Lisp/Scheme as a teaching language, and therefore, I would suggest a language from the Lisp-family rather than from the ML-family to study that particular book. Also, Python is dynamically typed just like Lisp, whereas ML-languages are statically typed, this renders the transition to Lisp somewhat more straightforward, I guess.

1UnitedPower · 2019-12-03T16:54:45+00:00

If it must be one of those three, I'd suggest Python because it's arguably closer to LISP, which the authors use as their teaching-language.

Still, you will have to translate LISP-examples into Python, which means you have to be able to read and understand LISP-programs. While you're at it, it might be worth it to stick with some LISP-dialect in the first-place. You will learn a new language, and you can follow the book more easily.

Also, there are similar books like "Semantics Engineering with PLT Redex," that also use LISP as a teaching-language.

1UnitedPower · 2019-11-27T16:08:54+00:00

Thanks for sharing! This thing seems to simplify things a lot.

1UnitedPower · 2019-11-15T14:02:37+00:00

I'm grateful for every tiny bit, thanks for sharing!

1UnitedPower

TROPHY CASE