3 ms·

I have some experience with Haskell [1], but I'm absolutely lost here. Can someone explain all this dependent-type syntax that's going on there, or would that b

I have some experience with Haskell [1], but I'm absolutely lost here. Can someone explain all this dependent-type syntax that's going on there, or would that be out of scope for a single comment? [1] The biggest Haskell program I wrote until now was a spellchecker as the final project for a university course.

gameswithgo 8y ago
At a very high level which you may have already found obvious, the type signature for the function basically says "this will take a list, and return a list that is sorted according to these rules, and is a permutation of the original list" basically proving that quicksort is correct at compile time.
danidiaz 8y ago
: is used for type annotations instead of :: like in Haskell. The double asterisk is syntactic sugar for a "dependent pair" http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-pairs http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... Basically, it is a pair in which the type of the second element depends on the value of the first element. Here it is being used to pack the result list with a proof that the list satisfies the required properties. The type of the proof must refer to the list, hence the need for dependent types. The stuff within braces {} are implicit arguments http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html?highlight=braces#implicit-arguments http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... that are not given explicitly, but are inferred from the type of other arguments. Type is commonly referred as the kind * in Haskell, the kind of types that have values. Unlike in vanilla Haskell, the types of data constructors are explicitly stated http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html?highlight=data#vectors http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... In Haskell the "types" of data constructors are kinds, and you need to enable the XKindSignatures extension to give them explicitly. https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?highlight=#extension-KindSignatures https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...
codebje 8y ago
I'll talk about this declaration only: data PreOrder : (a : Type) -> (a -> a -> Type) -> Type where PrO : {lte : a -> a -> Type} -- <= -> ((x : a) -> (y : a) -> (z : a) -> lte x y -> lte y z -> lte x z) -- transitivity -> PreOrder a lte This declares a function `PreOrder`, which when given some type called `a`, and some function from two `a`s to some other type, produces a type itself. The reason why we see `(a : Type)` to give a name to `a` is that the name is re-used in the second argument. To produce a value, a constructor is defined `PrO`, with one _implicit_ argument `lte` of type `a -> a -> Type` (note that this `a` is not the same `a` in the type for `PreOrder`!) that can be inferred from the other arguments, and one other argument of a complex type we'll dig into in a moment. If you supply `PrO` with these two things, you will get back an inhabitant of type `PreOrder a lte` - the type that `PreOrder` promises to return when given two things. This is the same as `Maybe` in Haskell being a type-level function, and `Maybe Int` being a type, where `Just` is a constructor that can produce a `Maybe Int` given an `Int`, and `Nothing` is a constructor that can also produce a `Maybe Int` out of nowhere. ((x : a) -> (y : a) -> (z : a) -> lte x y -> lte y z -> lte x z) This type is interesting because of the Curry-Howard correspondence, which basically says that types and propositions are the same thing, and expressions and proofs are the same thing. If you can show there exists some value of some type, you have proven the proposition the type represents. If you think about what `foo :: Int -> String` means in Haskell, you could turn it around to say "If there is an Int, then there is a String." Given some "proof" that `Int` is a non-empty type, that is, a value of type `Int`, can you prove that there exists some value of type `String`? Well, of course you can: `foo _ = "const"` is one such proof, as is `foo = show` or `foo x = if x < 10 then "less" else "greater"`. In Idris, we can express much more interesting types, such that the existence of some expression of that type is non-trivial. The above type signature is best viewed IMO as a predicate: ∀x, y, z ∈ a. x ≤ y ∧ y ≤ z ⇒ x ≤ z Remember that `a ⇒ b ⇒ c` is the same as `a ∧ b ⇒ c`, just curried, the type signature above is saying that given any x, y, z of type a, and some value indicating that `lte x y` is "true", and some value indicating that `lte y z` is "true", it can be shown that `lte x z` is "true" too. That is, a value of that type is a proof that `lte` is transitive. Given some _user supplied_ proof of transitivity, and the implicit transitive operator, we have an inhabitant of the type `PreOrder a lte`. This is dependently typed, because the _type_ of `lte x y` depends on the _value_ of `x` and `y`. When we say `lte : a -> a -> Type` we mean that `lte` is a function from two values of type `a` to some other type. As an example, we could write `badlte : Int -> Int -> Type; badlte _ _ = Int`. This comparison operator simply ignores its arguments and says the Type of all such comparisons is always `Int`, which is the same as saying that all `Int`s are equivalent, because the binary relation is inhabited for every possible pair of `Int`s. We can prove transitivity with the lambda expression `\x,y,z,ltexy,lteyz => 42`, that is, given three values and two proofs that x <= y and y <= z, we can "prove" x <= z because we can show there's an inhabitant for the type of `Int`. We can make a preorder, and a totalorder, and sort using this order (the result is that any permutation of the input list is fine, because everything's equivalent for comparison). As a more _interesting_ example, consider the definition of `LTE` for the type `Nat`: data LTE : (n, m : Nat) -> Type where LTEZero : LTE Z right LTESucc : LTE left right -> LTE (S left) (S right) This is an inductive type definition that depends on the values given. `Z`, or zero, the base case of a `Nat`, is less than or equal to every other value, so we can use `right` as a placeholder variable. Given the proof that `left <= right`, we can also say that the successor of `left` (`S left`) is less than the successor of `right`. This is a bog standard inductive proof form, transposed to code. `LTE` becomes a function from two `Nat`s to a `Type` - but it's a partial function, or relation, because not every `Nat` pair produces a `Type`. If we want to prove that 2 is less than or equal to 3, that is, `LTE 2 3`, we can construct it inductively: `LTESucc (LTESucc LTEZero)`, that is, given `0 <= 1` we can show `1 <= 2` and from that `2 <= 3`. But there's no way to chain `LTESucc` and `LTEZero` together to wind up with `LTE 3 2`.

gameswithgo 8y ago

At a very high level which you may have already found obvious, the type signature for the function basically says "this will take a list, and return a list that is sorted according to these rules, and is a permutation of the original list" basically proving that quicksort is correct at compile time.

danidiaz 8y ago

: is used for type annotations instead of :: like in Haskell. The double asterisk is syntactic sugar for a "dependent pair" http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-pairs http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... Basically, it is a pair in which the type of the second element depends on the value of the first element. Here it is being used to pack the result list with a proof that the list satisfies the required properties. The type of the proof must refer to the list, hence the need for dependent types. The stuff within braces {} are implicit arguments http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html?highlight=braces#implicit-arguments http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... that are not given explicitly, but are inferred from the type of other arguments. Type is commonly referred as the kind * in Haskell, the kind of types that have values. Unlike in vanilla Haskell, the types of data constructors are explicitly stated http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html?highlight=data#vectors http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... In Haskell the "types" of data constructors are kinds, and you need to enable the XKindSignatures extension to give them explicitly. https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?highlight=#extension-KindSignatures https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...

codebje 8y ago

I'll talk about this declaration only: data PreOrder : (a : Type) -> (a -> a -> Type) -> Type where PrO : {lte : a -> a -> Type} -- <= -> ((x : a) -> (y : a) -> (z : a) -> lte x y -> lte y z -> lte x z) -- transitivity -> PreOrder a lte This declares a function `PreOrder`, which when given some type called `a`, and some function from two `a`s to some other type, produces a type itself. The reason why we see `(a : Type)` to give a name to `a` is that the name is re-used in the second argument. To produce a value, a constructor is defined `PrO`, with one _implicit_ argument `lte` of type `a -> a -> Type` (note that this `a` is not the same `a` in the type for `PreOrder`!) that can be inferred from the other arguments, and one other argument of a complex type we'll dig into in a moment. If you supply `PrO` with these two things, you will get back an inhabitant of type `PreOrder a lte` - the type that `PreOrder` promises to return when given two things. This is the same as `Maybe` in Haskell being a type-level function, and `Maybe Int` being a type, where `Just` is a constructor that can produce a `Maybe Int` given an `Int`, and `Nothing` is a constructor that can also produce a `Maybe Int` out of nowhere. ((x : a) -> (y : a) -> (z : a) -> lte x y -> lte y z -> lte x z) This type is interesting because of the Curry-Howard correspondence, which basically says that types and propositions are the same thing, and expressions and proofs are the same thing. If you can show there exists some value of some type, you have proven the proposition the type represents. If you think about what `foo :: Int -> String` means in Haskell, you could turn it around to say "If there is an Int, then there is a String." Given some "proof" that `Int` is a non-empty type, that is, a value of type `Int`, can you prove that there exists some value of type `String`? Well, of course you can: `foo _ = "const"` is one such proof, as is `foo = show` or `foo x = if x < 10 then "less" else "greater"`. In Idris, we can express much more interesting types, such that the existence of some expression of that type is non-trivial. The above type signature is best viewed IMO as a predicate: ∀x, y, z ∈ a. x ≤ y ∧ y ≤ z ⇒ x ≤ z Remember that `a ⇒ b ⇒ c` is the same as `a ∧ b ⇒ c`, just curried, the type signature above is saying that given any x, y, z of type a, and some value indicating that `lte x y` is "true", and some value indicating that `lte y z` is "true", it can be shown that `lte x z` is "true" too. That is, a value of that type is a proof that `lte` is transitive. Given some _user supplied_ proof of transitivity, and the implicit transitive operator, we have an inhabitant of the type `PreOrder a lte`. This is dependently typed, because the _type_ of `lte x y` depends on the _value_ of `x` and `y`. When we say `lte : a -> a -> Type` we mean that `lte` is a function from two values of type `a` to some other type. As an example, we could write `badlte : Int -> Int -> Type; badlte _ _ = Int`. This comparison operator simply ignores its arguments and says the Type of all such comparisons is always `Int`, which is the same as saying that all `Int`s are equivalent, because the binary relation is inhabited for every possible pair of `Int`s. We can prove transitivity with the lambda expression `\x,y,z,ltexy,lteyz => 42`, that is, given three values and two proofs that x <= y and y <= z, we can "prove" x <= z because we can show there's an inhabitant for the type of `Int`. We can make a preorder, and a totalorder, and sort using this order (the result is that any permutation of the input list is fine, because everything's equivalent for comparison). As a more _interesting_ example, consider the definition of `LTE` for the type `Nat`: data LTE : (n, m : Nat) -> Type where LTEZero : LTE Z right LTESucc : LTE left right -> LTE (S left) (S right) This is an inductive type definition that depends on the values given. `Z`, or zero, the base case of a `Nat`, is less than or equal to every other value, so we can use `right` as a placeholder variable. Given the proof that `left <= right`, we can also say that the successor of `left` (`S left`) is less than the successor of `right`. This is a bog standard inductive proof form, transposed to code. `LTE` becomes a function from two `Nat`s to a `Type` - but it's a partial function, or relation, because not every `Nat` pair produces a `Type`. If we want to prove that 2 is less than or equal to 3, that is, `LTE 2 3`, we can construct it inductively: `LTESucc (LTESucc LTEZero)`, that is, given `0 <= 1` we can show `1 <= 2` and from that `2 <= 3`. But there's no way to chain `LTESucc` and `LTEZero` together to wind up with `LTE 3 2`.